1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Dec 07 16:14:32 2023 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Dec 07 17:16:22 2023 +0100
1.3 @@ -18,39 +18,7 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -(*T_POSold*)
1.8 -fun xml_of_itm_ (I_Model.Cor (dts, _)) =
1.9 - XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
1.10 - | xml_of_itm_ (I_Model.Syn c) =
1.11 - XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
1.12 - | xml_of_itm_ (I_Model.Typ c) =
1.13 - XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
1.14 - (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
1.15 - | xml_of_itm_ (I_Model.Inc (dts, _)) =
1.16 - XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
1.17 - | xml_of_itm_ (I_Model.Sup dts) =
1.18 - XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
1.19 - | xml_of_itm_ (I_Model.Mis (d, pid)) =
1.20 - XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
1.21 - | xml_of_itm_ _ = raise ERROR "xml_of_itm_: wrong argument"
1.22 -fun xml_of_itms itms =
1.23 - let
1.24 - fun extract (_, _, _, _, itm_) = itm_
1.25 - in map (xml_of_itm_ o extract) itms end
1.26 -(*T_POS*)
1.27 -fun xml_of_itm_POS (I_Model.Cor_POS dts) =
1.28 - XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
1.29 - | xml_of_itm_POS (I_Model.Syn_POS c) =
1.30 - XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
1.31 - | xml_of_itm_POS (I_Model.Inc_POS dts) =
1.32 - XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
1.33 - | xml_of_itm_POS (I_Model.Sup_POS dts) =
1.34 - XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
1.35 -fun xml_of_itms_POS itms =
1.36 - let
1.37 - fun extract (_, _, _, _, itm_) = itm_
1.38 - in map (xml_of_itm_POS o extract) itms end
1.39 -(*T_POSnew*)
1.40 +
1.41 \<close> ML \<open>
1.42 \<close>
1.43 end
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Dec 07 16:14:32 2023 +0100
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Dec 07 17:16:22 2023 +0100
2.3 @@ -287,7 +287,7 @@
2.4 XML.Elem (("STATUS", []), [
2.5 XML.Text ((if model_ok then "correct" else "incorrect"))]),
2.6 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),
2.7 - xml_of_model pbl where_])
2.8 + xml_of_model (I_Model.TEST_to_OLD pbl) where_])
2.9
2.10 fun xml_of_matchmet (model_ok, pI, program, pbl, where_) =
2.11 XML.Elem (("CONTEXTDATA", []), [
3.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 07 16:14:32 2023 +0100
3.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 07 17:16:22 2023 +0100
3.3 @@ -15,7 +15,7 @@
3.4 val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
3.5 val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T
3.6 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
3.7 - val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
3.8 + val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T_POS * Pre_Conds.T
3.9 end
3.10
3.11 (**)
3.12 @@ -174,14 +174,14 @@
3.13 |> Know_Store.get_via_last_thy
3.14 |> Proof_Context.init_global
3.15 in
3.16 - case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI (probl) of
3.17 + case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI (I_Model.OLD_to_POS probl) of
3.18 NONE => (*copy from context_pbl*)
3.19 let
3.20 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
3.21 val (_, (pbl, where_)) = M_Match.by_i_models ctxt os
3.22 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
3.23 in
3.24 - (false, pI, hdl, I_Model.TEST_to_OLD pbl, where_)
3.25 + (false, pI, hdl, pbl, where_)
3.26 end
3.27 | SOME (pI, (pbl, where_)) => (true, pI, hdl, pbl, where_)
3.28 end
4.1 --- a/src/Tools/isac/Specify/Specify.thy Thu Dec 07 16:14:32 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Thu Dec 07 17:16:22 2023 +0100
4.3 @@ -26,8 +26,6 @@
4.4
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 -Refine.problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
4.8 -\<close> ML \<open>
4.9
4.10 \<close> ML \<open>
4.11 \<close>
5.1 --- a/src/Tools/isac/Specify/cas-command.sml Thu Dec 07 16:14:32 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/cas-command.sml Thu Dec 07 17:16:22 2023 +0100
5.3 @@ -57,7 +57,7 @@
5.4 if mI <> ["no_met"]
5.5 then (pI, mI)
5.6 else
5.7 - case Refine.problem thy pI pits of
5.8 + case Refine.problem thy pI (I_Model.OLD_to_POS pits) of
5.9 SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
5.10 | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
5.11 val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI
6.1 --- a/src/Tools/isac/Specify/refine.sml Thu Dec 07 16:14:32 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/refine.sml Thu Dec 07 17:16:22 2023 +0100
6.3 @@ -28,25 +28,26 @@
6.4
6.5 signature REFINE_PROBLEM =
6.6 sig
6.7 -(**)
6.8 - val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
6.9 + val problem: theory -> Problem.id -> I_Model.T_POS -> (Problem.id * (I_Model.T_POS * Pre_Conds.T)) option
6.10
6.11 val by_o_model : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
6.12 val by_o_model' : Proof.context -> O_Model.T -> Problem.id -> Problem.id
6.13 val by_formalise: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list
6.14
6.15 (*from isac_test for Minisubpbl*)
6.16 - datatype match_model_prec = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_;
6.17 - val find_match: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node -> match_model_prec list
6.18 + type match_model_prec
6.19 + val find_match: theory -> Problem.id -> I_Model.T_POS -> match_model_prec list ->
6.20 + Problem.T Store.node -> match_model_prec list
6.21 val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
6.22 val check_match: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node ->
6.23 Problem.id option
6.24 val refins: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node list ->
6.25 Problem.id option
6.26 + val match_found: match_model_prec list -> match_model_prec option
6.27 + val find_matchs: theory -> Problem.id -> I_Model.T_POS -> match_model_prec list -> Problem.T Store.node list -> match_model_prec list
6.28
6.29 \<^isac_test>\<open>
6.30 - val match_found: match_model_prec list -> match_model_prec option
6.31 - val find_matchs: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node list -> match_model_prec list
6.32 +(**)
6.33 \<close>
6.34 end
6.35
6.36 @@ -56,7 +57,7 @@
6.37 (**)
6.38
6.39 datatype match_model_prec =
6.40 - Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
6.41 + Match_ of Problem.id * (( I_Model.T_POS) * (Pre_Conds.T))
6.42 | NoMatch_;
6.43
6.44 fun is_matches_ (Match_ _) = true
6.45 @@ -64,11 +65,12 @@
6.46 fun match_found ms = ((find_first is_matches_) o rev) ms;
6.47
6.48 (* version for tactic Refine_Problem *)
6.49 +(*OLD*)
6.50 fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
6.51 let
6.52 val {thy, model, where_, where_rls, ...} = py
6.53 val ctxt = Proof_Context.init_global thy
6.54 - val (b, where_') = M_Match.by_i_model ctxt (I_Model.OLD_to_POS itms) (model, where_, where_rls);
6.55 + val (b, where_') = M_Match.by_i_model ctxt itms (model, where_, where_rls);
6.56 in
6.57 if b
6.58 then pbls @ [Match_ (rev (pblRD @ [pI]), (itms, where_'))]
6.59 @@ -78,7 +80,7 @@
6.60 let
6.61 val {thy, model, where_, where_rls, ...} = py
6.62 val ctxt = Proof_Context.init_global thy
6.63 - val (b, where_') = M_Match.by_i_model ctxt (I_Model.OLD_to_POS itms) (model, where_, where_rls);
6.64 + val (b, where_') = M_Match.by_i_model ctxt itms (model, where_, where_rls);
6.65 in if b then
6.66 let val pbl = Match_ (rev (pblRD @ [pI]), (itms, where_'))
6.67 in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
7.1 --- a/src/Tools/isac/Specify/specify-step.sml Thu Dec 07 16:14:32 2023 +0100
7.2 +++ b/src/Tools/isac/Specify/specify-step.sml Thu Dec 07 17:16:22 2023 +0100
7.3 @@ -60,14 +60,14 @@
7.4 | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
7.5 val thy = if dI' = ThyC.id_empty then dI else dI';
7.6 in
7.7 - case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
7.8 + case Refine.problem (ThyC.get_theory ctxt thy) pI (I_Model.OLD_to_POS itms) of
7.9 NONE => Applicable.No
7.10 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
7.11 | SOME (pI', (i_model, prec)) =>
7.12 if pI' = pI
7.13 then Applicable.No
7.14 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
7.15 - else Applicable.Yes (Tactic.Refine_Problem' (pI', (I_Model.OLD_to_POS i_model, prec)))
7.16 + else Applicable.Yes (Tactic.Refine_Problem' (pI', (i_model, prec)))
7.17 end
7.18 | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
7.19 let
8.1 --- a/src/Tools/isac/Specify/step-specify.sml Thu Dec 07 16:14:32 2023 +0100
8.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu Dec 07 17:16:22 2023 +0100
8.3 @@ -72,14 +72,14 @@
8.4 | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
8.5 val thy = if dI' = ThyC.id_empty then dI else dI'
8.6 in
8.7 - case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
8.8 + case Refine.problem (ThyC.get_theory ctxt thy) pI (I_Model.OLD_to_POS probl) of
8.9 NONE => ("failure", ([], [], ptp))
8.10 | SOME (pI, (i_model, prec)) =>
8.11 let
8.12 - val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' (pI, (I_Model.OLD_to_POS i_model, prec)) )
8.13 + val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' (pI, (i_model, prec)) )
8.14 (Istate_Def.Uistate, ctxt) (pt, pos)
8.15 in
8.16 - ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' (pI, (I_Model.OLD_to_POS i_model, prec)),
8.17 + ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' (pI, (i_model, prec)),
8.18 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
8.19 end
8.20 end