walther@59960: (* Title: Specify/refine.sml walther@59960: Author: Walther Neuper 110226 walther@59960: (c) due to copyright terms walther@59960: Walther@60555: Refine a problem by a search for a \ML_structure Model_Pattern\ Walther@60586: better fitting the respective where_-condition. Walther@60555: Walther@60658: The search on the tree given by @{term Know_Store.get_pbls} is costly such that Walther@60658: \ML_structure Know_Store\ holds terms pre-parsed with a most generally type. Walther@60658: Walther@60658: On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type Walther@60658: (and users of this function in \ML_structure Error_Pattern, MethodC, Problem\) Walther@60658: according to the current context. Walther@60555: Walther@60555: Note: From the children of eb89f586b0b2 onwards the old functions (\term TermC.typ_a2real\ etc) Walther@60555: are adapted for "adapt_to_type on the fly" until further clarification. Walther@60556: Walther@60556: timing (from evaluating imports to use-cases.sml) for Test_Isac_Short Walther@60556: before adapt_to_type: 01:05 sec:sec Walther@60556: after adapt_to_type: Walther@60556: timing for test/../refine.sml --- equation with CalcTree [ = 6 / 5] for timing: ... Walther@60556: before adapt_to_type: 1.5 sec Walther@60556: after adapt_to_type: Walther@60556: timing for test/../refine.sml --- refine ad-hoc equation for timing: ... Walther@60556: before adapt_to_type: 0.05 sec Walther@60556: after adapt_to_type: Walther@60556: *) walther@59960: walther@59960: signature REFINE_PROBLEM = walther@59960: sig Walther@60556: (**) walther@59968: val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option walther@59968: Walther@60742: val by_o_model : Proof.context -> O_Model.T -> Problem.id -> Problem.id option Walther@60742: val by_o_model' : Proof.context -> O_Model.T -> Problem.id -> Problem.id Walther@60742: val by_formalise: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list walther@59960: Walther@60729: (*from isac_test for Minisubpbl*) Walther@60742: datatype match_model_prec = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_; Walther@60742: val find_match: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node -> match_model_prec list Walther@60742: val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a Walther@60742: val check_match: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option Walther@60736: Walther@60736: \<^isac_test>\ Walther@60742: val match_found: match_model_prec list -> match_model_prec option Walther@60742: val find_matchs: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node list -> match_model_prec list wenzelm@60223: \ walther@59960: end walther@59960: walther@59965: (**) walther@59960: structure Refine(**) : REFINE_PROBLEM(**) = walther@59960: struct walther@59965: (**) walther@59960: Walther@60742: datatype match_model_prec = walther@59963: Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) walther@59960: | NoMatch_; walther@59960: walther@59960: fun is_matches_ (Match_ _) = true walther@59960: | is_matches_ _ = false; walther@59960: Walther@60742: fun match_found ms = ((find_first is_matches_) o rev) ms; walther@59960: walther@59960: fun eq1 d (_, (d', _)) = (d = d'); walther@59960: Walther@60478: (* chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*) Walther@60745: (*T_TESTold*) walther@59960: fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) = walther@59960: (case find_first (eq1 d) pbt of Walther@60478: SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)]))) walther@59960: | NONE => (i, vats, false, f, I_Model.Sup (d, vs))) walther@59960: | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) = walther@59960: (case find_first (eq1 d) pbt of Walther@60478: SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)]))) walther@59960: | NONE => (i, vats, false, f, I_Model.Sup (d, vs))) walther@59960: | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm walther@59960: | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm walther@59960: | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) = walther@59960: (case find_first (eq1 d) pbt of Walther@60478: SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)]))) walther@59960: | NONE => (i, vats, false, f, I_Model.Sup (d, vs))) walther@59960: | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) = walther@59960: (case find_first (eq1 d) pbt of Walther@60478: SOME _ => Walther@60478: raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)" walther@59960: | NONE => (i, vats, false, f, I_Model.Sup (d, [vs]))) walther@59960: | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def."; Walther@60745: (*T_TEST*) Walther@60745: fun chk_TEST (_: theory) pbt (i, vats, b, f, I_Model.Cor_TEST ((d, vs), _)) = Walther@60745: (case find_first (eq1 d) pbt of Walther@60745: SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST ((d, vs), (id, [Input_Descript.join'''' (d, vs)]))) Walther@60745: | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs))) Walther@60745: | chk_TEST _ pbt (i, vats, b, f, I_Model.Inc_TEST ((d, vs), _)) = Walther@60745: (case find_first (eq1 d) pbt of Walther@60745: SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST ((d, vs), (id, [Input_Descript.join'''' (d, vs)]))) Walther@60745: | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs))) Walther@60745: | chk_TEST _ pbt (i, vats, b, f, I_Model.Sup_TEST (d, vs)) = Walther@60745: (case find_first (eq1 d) pbt of Walther@60745: SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST ((d,vs), (id, [Input_Descript.join'''' (d, vs)]))) Walther@60745: | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs))) Walther@60745: (*T_TESTnew*) walther@59960: Walther@60477: fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; walther@59960: fun eq0 (0, _, _, _, _) = true walther@59960: | eq0 _ = false; walther@59960: fun max_i i [] = i walther@59960: | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is; walther@59960: fun max_id [] = 0 walther@59960: | max_id ((id, _, _, _, _) :: is) = max_i id is; walther@59960: fun add_idvat itms _ _ [] = itms walther@59960: | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) = walther@59960: add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its; walther@59960: walther@59960: (* find elements of pbt not contained in itms; walther@59960: if such one is untouched, return this one, otherwise create new itm *) walther@59960: fun chk_m itms untouched (p as (f, (d, id))) = walther@59960: case find_first (eq2 p) itms of walther@59960: SOME _ => [] walther@59960: | NONE => walther@59960: (case find_first (eq2 p) untouched of walther@59960: SOME itm => [itm] walther@59960: | NONE => [(0, [], false, f, I_Model.Mis (d, id))]); walther@59960: walther@59960: fun chk_mis mvat itms untouched pbt = walther@59960: let val mis = (flat o (map (chk_m itms untouched))) pbt; walther@59960: val mid = max_id itms; walther@59960: in add_idvat [] (mid + 1) mvat mis end; walther@59960: walther@59960: (* check a problem (ie. itm list) for matching a problemtype, Walther@60705: takes the Pre_Conds.max_variant for concluding completeness (could be another!) *) Walther@60729: fun match_itms thy itms (pbt, where_, where_rls) = Walther@60729: let Walther@60729: fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b; Walther@60729: val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *) Walther@60729: val mvat = Pre_Conds.max_variant itms'; Walther@60729: val itms'' = filter (okv mvat) itms'; Walther@60729: val untouched = filter eq0 itms; (* i.e. dsc only (from init)*) Walther@60729: val mis = chk_mis mvat itms'' untouched pbt; Walther@60741: val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ Walther@60729: (pbt, I_Model.OLD_to_TEST itms'') Walther@60729: in (length mis = 0 andalso pb, (itms'@ mis, where_')) end; walther@59960: walther@59960: (* refine a problem; version for tactic Refine_Problem *) Walther@60742: fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) = walther@59960: let Walther@60585: val {thy, model, where_, where_rls, ...} = py Walther@60556: (*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*) Walther@60586: val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls); walther@59960: in walther@59960: if b Walther@60586: then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', where_'))] walther@59960: else pbls @ [NoMatch_] walther@59960: end Walther@60742: | find_match _ pblRD itms pbls (Store.Node (pI, [py], pys)) = walther@59960: let Walther@60585: val {thy, model, where_, where_rls, ...} = py Walther@60586: val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls); walther@59960: in if b Walther@60586: then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', where_')) Walther@60742: in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end walther@59960: else (pbls @ [NoMatch_]) Walther@60556: end Walther@60742: | find_match _ _ _ _ _ = raise ERROR "find_match: uncovered fun def." Walther@60742: and find_matchs _ _ _ pbls [] = pbls Walther@60742: | find_matchs thy pblRD itms pbls ((p as Store.Node _) :: pts) = walther@59960: let Walther@60742: val pbls' = find_match thy pblRD itms pbls p walther@59960: in case last_elem pbls' of walther@59960: Match_ _ => pbls' Walther@60742: | NoMatch_ => find_matchs thy pblRD itms pbls' pts walther@59960: end; walther@59960: walther@59960: fun problem thy pblID itms = Walther@60742: case match_found ((Store.apply (get_pbls ())) (find_match thy ((rev o tl) pblID) itms []) walther@60324: pblID (rev pblID)) of walther@59960: NONE => NONE Walther@60556: | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd; walther@59960: Walther@60556: (* Walther@60729: refine a problem; construct pblRD while scanning Problem.T Store.T Walther@60742: TODO: as \check_match: 'a -> .. -> 'b option\ could be ignorant of Store.T structure. Walther@60556: *) Walther@60742: fun check_match ctxt pblRD ori (Store.Node (pI, [py], [])) = Walther@60556: let Walther@60742: val _ = writeln ("check_match 1: " ^ strs2str pblRD) Walther@60585: val {where_rls, model, where_, ...} = py: Problem.T Walther@60585: val model = map (Model_Pattern.adapt_to_type ctxt) model Walther@60660: val where_ = map (ParseC.adapt_term_to_type ctxt) where_ Walther@60556: in Walther@60590: if M_Match.match_oris ctxt where_rls ori (model, where_) Walther@60729: then SOME (pblRD(**) @ [pI](**)) Walther@60556: else NONE Walther@60556: end Walther@60742: | check_match ctxt pblRD ori (Store.Node (pI, [py], pys)) = Walther@60556: let Walther@60742: val _ = writeln ("check_match 2: " ^ strs2str pblRD) Walther@60585: val {where_rls, model, where_, ...} = py: Problem.T Walther@60585: val model = map (Model_Pattern.adapt_to_type ctxt) model Walther@60660: val where_ = map (ParseC.adapt_term_to_type ctxt) where_ Walther@60556: in Walther@60590: if M_Match.match_oris ctxt where_rls ori (model, where_) Walther@60575: then (case refins ctxt (pblRD @ [pI]) ori pys of Walther@60556: SOME pblRD' => SOME pblRD' Walther@60729: | NONE => SOME (pblRD (**)@ [pI](**))) Walther@60556: else NONE Walther@60556: end Walther@60742: | check_match _ _ _ _ = raise ERROR "check_match: uncovered fun def." Walther@60575: and refins _ _ _ [] = NONE Walther@60575: | refins ctxt pblRD ori ((p as Store.Node _) :: pts) = Walther@60729: (writeln ("refins: " ^ strs2str pblRD); Walther@60742: (case check_match ctxt pblRD ori p of Walther@60729: SOME pblRD' => SOME (pblRD') Walther@60729: | NONE => refins ctxt pblRD ori pts) Walther@60729: ); Walther@60556: Walther@60556: \<^isac_test>\ Walther@60738: (**) Walther@60738: \ Walther@60738: Walther@60729: (* refine a problem; version providing output for math authors *) Walther@60575: (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list -> Walther@60556: Probl_Def.T Store.node -> M_Match.T list*) Walther@60575: fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) = Walther@60556: let Walther@60556: val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI]) Walther@60585: val {thy, model, where_, where_rls, ...} = py Walther@60585: val model = map (Model_Pattern.adapt_to_type ctxt) model Walther@60660: val where_ = map (ParseC.adapt_term_to_type ctxt) where_ Walther@60653: val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*) Walther@60586: val (b, (itms, where_')) = Walther@60585: M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls) Walther@60653: in Walther@60556: if b Walther@60586: then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')] Walther@60586: else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')] Walther@60556: end Walther@60575: | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) = Walther@60556: let Walther@60556: val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI]) Walther@60585: val {thy, model, where_, where_rls, ...} = py Walther@60585: val model = map (Model_Pattern.adapt_to_type ctxt) model Walther@60660: val where_ = map (ParseC.adapt_term_to_type ctxt) where_ Walther@60653: val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*) Walther@60586: val (b, (itms, where_')) = Walther@60585: M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls) Walther@60556: in Walther@60556: if b Walther@60556: then Walther@60586: let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_') Walther@60575: in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end Walther@60586: else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]) Walther@60556: end Walther@60575: | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def." Walther@60575: and refins' _ _ _ pbls [] = pbls Walther@60575: | refins' ctxt pblRD fmz pbls ((p as Store.Node _) :: pts) = Walther@60556: let Walther@60575: val pbls' = refin' ctxt pblRD fmz pbls p Walther@60556: in Walther@60556: case last_elem pbls' of Walther@60556: M_Match.Matches _ => pbls' Walther@60575: | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts Walther@60556: end; walther@59968: Walther@60556: (* Walther@60556: TODO: rename \ apply_to_node Walther@60556: apply a fun to a ptyps node. Walther@60742: val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a Walther@60729: TODO: Store.apply scans Store.T only to the first hit; see Store.apply. Walther@60556: *) Walther@60742: fun find_node_elem x = Store.apply (get_pbls ()) x; walther@59968: Walther@60742: (*for tactic Refine_Tacitly; oris are already created wrt. some pbt; ctxt overrides thy in pbt*) Walther@60742: fun by_o_model ctxt oris pblID = walther@59968: let Walther@60742: val opt = find_node_elem (check_match ctxt ((rev o tl) pblID) oris) pblID (rev pblID); Walther@60556: in case opt of walther@59968: SOME pblRD => walther@59968: let val pblID': Problem.id = rev pblRD walther@59968: in if pblID' = pblID then NONE else SOME pblID' end walther@59968: | NONE => NONE walther@59968: end; Walther@60742: fun by_o_model' ctxt oris pI = perhaps (by_o_model ctxt oris) pI; Walther@60742: Walther@60742: (*specifically for tests*) Walther@60742: fun by_formalise ctxt fmz pblID = Walther@60742: find_node_elem (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID); walther@59968: walther@60268: \<^isac_test>\ Walther@60738: (**) walther@60268: \ walther@59968: walther@59965: (**)end(**)