prep. cleanup of Specification
1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri May 15 11:46:43 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri May 15 14:22:05 2020 +0200
1.3 @@ -424,9 +424,9 @@
1.4 (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
1.5 XML.Elem (("FIND", []), finds),
1.6 XML.Elem (("RELATE", []), relates)])) =
1.7 - ([P_Specific.Given (map xml_to_cterm givens),
1.8 - P_Specific.Find (map xml_to_cterm finds),
1.9 - P_Specific.Relate (map xml_to_cterm relates)]) : P_Specific.imodel
1.10 + ([P_Spec.Given (map xml_to_cterm givens),
1.11 + P_Spec.Find (map xml_to_cterm finds),
1.12 + P_Spec.Relate (map xml_to_cterm relates)]) : P_Spec.imodel
1.13 | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
1.14 fun xml_to_icalhd
1.15 (XML.Elem (( "ICALCHEAD", []), [
1.16 @@ -436,7 +436,7 @@
1.17 XML.Elem (( "POS", []), [XML.Text belongsto]),
1.18 spec as XML.Elem (( "SPECIFICATION", []), _)])) =
1.19 (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel,
1.20 - Pos.str2pos_ belongsto, xml_to_spec spec) : P_Specific.icalhd
1.21 + Pos.str2pos_ belongsto, xml_to_spec spec) : P_Spec.icalhd
1.22 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
1.23
1.24 fun xml_of_sub (id, value) =
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri May 15 11:46:43 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Fri May 15 14:22:05 2020 +0200
2.3 @@ -31,7 +31,7 @@
2.4 val Iterator : calcID -> XML.tree
2.5 val IteratorTEST : calcID -> iterID
2.6 val modelProblem : calcID -> XML.tree
2.7 - val modifyCalcHead : calcID -> P_Specific.icalhd -> XML.tree
2.8 + val modifyCalcHead : calcID -> P_Spec.icalhd -> XML.tree
2.9 val moveActiveCalcHead : calcID -> XML.tree
2.10 val moveActiveDown : calcID -> XML.tree
2.11 val moveActiveFormula : calcID -> Pos.pos' -> XML.tree
2.12 @@ -73,12 +73,12 @@
2.13 called for each cterm', icalhd, fmz in this interface;
2.14 + see "fun en/decode" in /mathml.sml *)
2.15 fun encode_imodel imodel =
2.16 - let fun enc (P_Specific.Given ifos) = P_Specific.Given (map encode ifos)
2.17 - | enc (P_Specific.Find ifos) = P_Specific.Find (map encode ifos)
2.18 - | enc (P_Specific.Relate ifos) = P_Specific.Relate (map encode ifos)
2.19 - in map enc imodel:P_Specific.imodel end;
2.20 -fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Specific.icalhd) =
2.21 - (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Specific.icalhd;
2.22 + let fun enc (P_Spec.Given ifos) = P_Spec.Given (map encode ifos)
2.23 + | enc (P_Spec.Find ifos) = P_Spec.Find (map encode ifos)
2.24 + | enc (P_Spec.Relate ifos) = P_Spec.Relate (map encode ifos)
2.25 + in map enc imodel:P_Spec.imodel end;
2.26 +fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Spec.icalhd) =
2.27 + (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Spec.icalhd;
2.28 fun encode_fmz (ifos, spec) = (map encode ifos, spec);
2.29
2.30
2.31 @@ -288,10 +288,10 @@
2.32 end)
2.33 handle _ => sysERROR2xml cI "error in kernel 8";
2.34
2.35 -fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Specific.icalhd) =
2.36 +fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) =
2.37 (let
2.38 val ((pt,_),_) = get_calc cI
2.39 - val (pt, chd as (_,p_,_,_,_,_)) = P_Specific.input_icalhd pt ichd
2.40 + val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd
2.41 in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
2.42 handle _ => sysERROR2xml cI "error in kernel 9";
2.43
3.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 15 11:46:43 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 15 14:22:05 2020 +0200
3.3 @@ -148,7 +148,7 @@
3.4 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
3.5 else pI'
3.6 val {ppc, where_, prls, ...} = Problem.from_store pblID
3.7 - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
3.8 + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
3.9 in
3.10 (model_ok, pblID, hdl, pbl, pre)
3.11 end
3.12 @@ -163,7 +163,7 @@
3.13 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
3.14 else mI'
3.15 val {ppc, pre, prls, scr, ...} = Method.from_store metID
3.16 - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
3.17 + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
3.18 in
3.19 (model_ok, metID, scr, pbl, pre)
3.20 end
3.21 @@ -176,7 +176,7 @@
3.22 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
3.23 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
3.24 val {ppc,where_,prls,...} = Problem.from_store pI
3.25 - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
3.26 + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
3.27 in
3.28 (model_ok, pI, hdl, pbl, pre)
3.29 end
3.30 @@ -188,7 +188,7 @@
3.31 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
3.32 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
3.33 val {ppc,pre,prls,scr,...} = Method.from_store mI
3.34 - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
3.35 + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
3.36 in
3.37 (model_ok, mI, scr, pbl, pre)
3.38 end
3.39 @@ -204,7 +204,7 @@
3.40 NONE => (*copy from context_pbl*)
3.41 let
3.42 val {ppc,where_,prls,...} = Problem.from_store pI
3.43 - val (_, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
3.44 + val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
3.45 in
3.46 (false, pI, hdl, pbl, pre)
3.47 end
4.1 --- a/src/Tools/isac/Specify/Specify.thy Fri May 15 11:46:43 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Fri May 15 14:22:05 2020 +0200
4.3 @@ -12,13 +12,13 @@
4.4 ML_file "i-model.sml"
4.5 ML_file "pre-conditions.sml"
4.6 ML_file "p-model.sml"
4.7 - ML_file model.sml
4.8 + ML_file "m-match.sml"
4.9 ML_file refine.sml
4.10 ML_file "test-out.sml"
4.11 ML_file "specify-step.sml"
4.12 ML_file specification.sml
4.13 ML_file "cas-command.sml"
4.14 - ML_file "p-specific.sml"
4.15 + ML_file "p-spec.sml"
4.16 ML_file specify.sml
4.17 ML_file "step-specify.sml"
4.18
5.1 --- a/src/Tools/isac/Specify/formalise.sml Fri May 15 11:46:43 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/formalise.sml Fri May 15 14:22:05 2020 +0200
5.3 @@ -1,6 +1,11 @@
5.4 -(* Title: MathEngBasic/calc-tree-elem.sml
5.5 +(* Title: Specify/formalise.sml
5.6 Author: Walther Neuper 191026
5.7 (c) due to copyright terms
5.8 +
5.9 +A formalisation contains all data requred to solve a calculation.
5.10 +Specifically in the root of a calculation the formalisation might contain items,
5.11 +which are required by Subproblem's (e.g. "errorBound" in case an equation
5.12 +cannot be solved symbolically and thus is solved numerically)
5.13 *)
5.14 signature FORMALISE =
5.15 sig
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/isac/Specify/m-match.sml Fri May 15 14:22:05 2020 +0200
6.3 @@ -0,0 +1,143 @@
6.4 +(* Title: Specify/model.sml
6.5 + Author: Walther Neuper 110226
6.6 + (c) due to copyright terms
6.7 +
6.8 +Operations on models.
6.9 +*)
6.10 +
6.11 +signature MODEL_MATCH =
6.12 +sig
6.13 + datatype T =
6.14 + Matches of Problem.id * P_Model.T
6.15 + | NoMatch of Problem.id * P_Model.T
6.16 + val matchs2str : T list -> string
6.17 +
6.18 + val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
6.19 +(*unify ^^^^^^^^^^ vvvvvvvvvv
6.20 + vvvvvvvvv ^^^^^^^^^*)
6.21 + val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
6.22 + bool * (I_Model.T * Pre_Conds.T)
6.23 + val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
6.24 + O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
6.25 +
6.26 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.27 + datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
6.28 + val match_pbl : Formalise.model -> Problem.T -> match'
6.29 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.30 + (*NONE*)
6.31 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.32 +end
6.33 +
6.34 +(**)
6.35 +structure M_Match(**) : MODEL_MATCH(**) =
6.36 +struct
6.37 +(**)
6.38 +
6.39 +datatype T =
6.40 + Matches of Problem.id * P_Model.T
6.41 +| NoMatch of Problem.id * P_Model.T;
6.42 +fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"
6.43 + | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")";
6.44 +fun matchs2str ms = (strs2str o (map match2str)) ms;
6.45 +
6.46 +
6.47 +fun field_eq f (_, _, f', _, _) = f = f';
6.48 +
6.49 +fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
6.50 +fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
6.51 +fun eq1 d (_, (d', _)) = (d = d');
6.52 +
6.53 +fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
6.54 +
6.55 +(* check an ori for matching a problemtype by description;
6.56 + returns true only for itms found in pbt *)
6.57 +fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
6.58 + case find_first (eq1 d) pbt of
6.59 + SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))]
6.60 + | NONE => [];
6.61 +
6.62 +(* elem 'p' of pbt contained in itms ? *)
6.63 +fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
6.64 +fun chk1_m' oris (p as (f, (d, t))) =
6.65 + case find_first (eq2' p) oris of
6.66 + SOME _ => []
6.67 + | NONE => [(f, I_Model.Mis (d, t))];
6.68 +fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
6.69 +
6.70 +fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
6.71 +fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
6.72 +
6.73 +(* check a problem (ie. ori list) for matching a problemtype,
6.74 + takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
6.75 +fun match_oris thy prls oris (pbt,pre) =
6.76 + let
6.77 + val itms = (flat o (map (chk1_ thy pbt))) oris;
6.78 + val mvat = I_Model.vars_of itms;
6.79 + val complete = chk1_mis mvat itms pbt;
6.80 + val pre' = Pre_Conds.check prls pre itms mvat;
6.81 + val pb = foldl and_ (true, map fst pre');
6.82 + in if complete andalso pb then true else false end;
6.83 +
6.84 +(* check a problem (ie. ori list) for matching a problemtype,
6.85 + returns items for output to math-experts *)
6.86 +fun match_oris' thy oris (ppc, pre, prls) =
6.87 + let
6.88 + val itms = (flat o (map (chk1_ thy ppc))) oris;
6.89 + val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
6.90 + val mvat = I_Model.vars_of itms;
6.91 + val miss = chk1_mis' oris ppc;
6.92 + val pre' = Pre_Conds.check prls pre itms mvat;
6.93 + val pb = foldl and_ (true, map fst pre');
6.94 + in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
6.95 +
6.96 +
6.97 +(** check a problem (ie. itm list) for matching a problemtype **)
6.98 +
6.99 +(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
6.100 + for missing items get data from formalization (ie. ori list);
6.101 + takes the I_Model.vars_of for concluding completeness (could be another!)
6.102 +
6.103 + (0) determine the most frequent variant mv in pbl
6.104 + ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
6.105 + (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
6.106 + (3) newitms = filter (mv mem vat(news)) news
6.107 + (4) pbt @ newitms *)
6.108 +fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
6.109 + let
6.110 + (*0*)val mv = I_Model.max_vt pbl;
6.111 +
6.112 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
6.113 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
6.114 + SOME _ => false | NONE => true;
6.115 + (*1*)val mis = (filter (notmem pbl)) pbt;
6.116 +
6.117 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
6.118 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
6.119 + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
6.120 + val news = (flat o (map (oris2itms oris))) mis;
6.121 + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
6.122 + val newitms = filter mem_vat news;
6.123 + (*4*)val itms' = pbl @ newitms;
6.124 + val pre' = Pre_Conds.check prls pre itms' mv;
6.125 + val pb = foldl and_ (true, map fst pre');
6.126 + in (length mis = 0 andalso pb, (itms', pre')) end;
6.127 +
6.128 +
6.129 +(** for use by math-authors **)
6.130 +
6.131 +datatype match' = (* for the user *)
6.132 + Matches' of P_Model.T
6.133 +| NoMatch' of P_Model.T;
6.134 +
6.135 +(* match a formalization with a problem type, for tests *)
6.136 +fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
6.137 + let
6.138 + val oris = O_Model.init fmz thy ppc(* |> #1*);
6.139 + val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
6.140 + in
6.141 + if bool
6.142 + then Matches' (P_Model.from thy itms pre')
6.143 + else NoMatch' (P_Model.from thy itms pre')
6.144 + end;
6.145 +
6.146 +(**)end(**)
7.1 --- a/src/Tools/isac/Specify/model.sml Fri May 15 11:46:43 2020 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,143 +0,0 @@
7.4 -(* Title: Specify/model.sml
7.5 - Author: Walther Neuper 110226
7.6 - (c) due to copyright terms
7.7 -
7.8 -Operations on models.
7.9 -*)
7.10 -
7.11 -signature MODEL =
7.12 -sig
7.13 - datatype match =
7.14 - Matches of Problem.id * P_Model.T
7.15 - | NoMatch of Problem.id * P_Model.T
7.16 - val matchs2str : match list -> string
7.17 -
7.18 - val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
7.19 -(*unify ^^^^^^^^^^ vvvvvvvvvv
7.20 - vvvvvvvvv ^^^^^^^^^*)
7.21 - val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
7.22 - bool * (I_Model.T * Pre_Conds.T)
7.23 - val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
7.24 - O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
7.25 -
7.26 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.27 - datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
7.28 - val match_pbl : Formalise.model -> Problem.T -> match'
7.29 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.30 - (*NONE*)
7.31 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.32 -end
7.33 -
7.34 -(**)
7.35 -structure Model(** ) : MODEL( **) =
7.36 -struct
7.37 -(**)
7.38 -
7.39 -datatype match =
7.40 - Matches of Problem.id * P_Model.T
7.41 -| NoMatch of Problem.id * P_Model.T;
7.42 -fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"
7.43 - | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")";
7.44 -fun matchs2str ms = (strs2str o (map match2str)) ms;
7.45 -
7.46 -
7.47 -fun field_eq f (_, _, f', _, _) = f = f';
7.48 -
7.49 -fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
7.50 -fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
7.51 -fun eq1 d (_, (d', _)) = (d = d');
7.52 -
7.53 -fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
7.54 -
7.55 -(* check an ori for matching a problemtype by description;
7.56 - returns true only for itms found in pbt *)
7.57 -fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
7.58 - case find_first (eq1 d) pbt of
7.59 - SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))]
7.60 - | NONE => [];
7.61 -
7.62 -(* elem 'p' of pbt contained in itms ? *)
7.63 -fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
7.64 -fun chk1_m' oris (p as (f, (d, t))) =
7.65 - case find_first (eq2' p) oris of
7.66 - SOME _ => []
7.67 - | NONE => [(f, I_Model.Mis (d, t))];
7.68 -fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
7.69 -
7.70 -fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
7.71 -fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
7.72 -
7.73 -(* check a problem (ie. ori list) for matching a problemtype,
7.74 - takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
7.75 -fun match_oris thy prls oris (pbt,pre) =
7.76 - let
7.77 - val itms = (flat o (map (chk1_ thy pbt))) oris;
7.78 - val mvat = I_Model.vars_of itms;
7.79 - val complete = chk1_mis mvat itms pbt;
7.80 - val pre' = Pre_Conds.check prls pre itms mvat;
7.81 - val pb = foldl and_ (true, map fst pre');
7.82 - in if complete andalso pb then true else false end;
7.83 -
7.84 -(* check a problem (ie. ori list) for matching a problemtype,
7.85 - returns items for output to math-experts *)
7.86 -fun match_oris' thy oris (ppc, pre, prls) =
7.87 - let
7.88 - val itms = (flat o (map (chk1_ thy ppc))) oris;
7.89 - val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
7.90 - val mvat = I_Model.vars_of itms;
7.91 - val miss = chk1_mis' oris ppc;
7.92 - val pre' = Pre_Conds.check prls pre itms mvat;
7.93 - val pb = foldl and_ (true, map fst pre');
7.94 - in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
7.95 -
7.96 -
7.97 -(** check a problem (ie. itm list) for matching a problemtype **)
7.98 -
7.99 -(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
7.100 - for missing items get data from formalization (ie. ori list);
7.101 - takes the I_Model.vars_of for concluding completeness (could be another!)
7.102 -
7.103 - (0) determine the most frequent variant mv in pbl
7.104 - ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
7.105 - (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
7.106 - (3) newitms = filter (mv mem vat(news)) news
7.107 - (4) pbt @ newitms *)
7.108 -fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
7.109 - let
7.110 - (*0*)val mv = I_Model.max_vt pbl;
7.111 -
7.112 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
7.113 - fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
7.114 - SOME _ => false | NONE => true;
7.115 - (*1*)val mis = (filter (notmem pbl)) pbt;
7.116 -
7.117 - fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
7.118 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
7.119 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
7.120 - val news = (flat o (map (oris2itms oris))) mis;
7.121 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
7.122 - val newitms = filter mem_vat news;
7.123 - (*4*)val itms' = pbl @ newitms;
7.124 - val pre' = Pre_Conds.check prls pre itms' mv;
7.125 - val pb = foldl and_ (true, map fst pre');
7.126 - in (length mis = 0 andalso pb, (itms', pre')) end;
7.127 -
7.128 -
7.129 -(** for use by math-authors **)
7.130 -
7.131 -datatype match' = (* for the user *)
7.132 - Matches' of P_Model.T
7.133 -| NoMatch' of P_Model.T;
7.134 -
7.135 -(* match a formalization with a problem type, for tests *)
7.136 -fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
7.137 - let
7.138 - val oris = O_Model.init fmz thy ppc(* |> #1*);
7.139 - val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
7.140 - in
7.141 - if bool
7.142 - then Matches' (P_Model.from thy itms pre')
7.143 - else NoMatch' (P_Model.from thy itms pre')
7.144 - end;
7.145 -
7.146 -(**)end(**)
8.1 --- a/src/Tools/isac/Specify/o-model.sml Fri May 15 11:46:43 2020 +0200
8.2 +++ b/src/Tools/isac/Specify/o-model.sml Fri May 15 14:22:05 2020 +0200
8.3 @@ -2,7 +2,7 @@
8.4 Author: Walther Neuper 110226
8.5 (c) due to copyright terms
8.6
8.7 -Original model created initially from Formale.T and Model_Pattern.T;
8.8 +An original model is created initially from Formalise.T and Model_Pattern.T;
8.9 This model makes student's editing via I_Model.T more efficient.
8.10 TODO: revise with an example with more than 1 variant.
8.11 *)
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/isac/Specify/p-spec.sml Fri May 15 14:22:05 2020 +0200
9.3 @@ -0,0 +1,247 @@
9.4 +(* Title: Specify/input-calchead.sml
9.5 + Author: Walther Neuper
9.6 + (c) due to copyright terms
9.7 +
9.8 +This will be dropped at switch to Isabelle/PIDE.
9.9 +*)
9.10 +
9.11 +signature PRESENTATION_SPECIFICATION =
9.12 +sig
9.13 + datatype iitem =
9.14 + Find of TermC.as_string list
9.15 + | Given of TermC.as_string list
9.16 + | Relate of TermC.as_string list
9.17 + type imodel = iitem list
9.18 + type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
9.19 + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
9.20 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.21 + (* NONE *)
9.22 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.23 + val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
9.24 + string * TermC.as_string -> I_Model.single
9.25 + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
9.26 + (string * TermC.as_string) list -> I_Model.T
9.27 + val e_icalhd: icalhd
9.28 + val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
9.29 + val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
9.30 + val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
9.31 + int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
9.32 + val imodel2fstr: iitem list -> (string * TermC.as_string) list
9.33 + val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
9.34 + val is_e_ts: term list -> bool
9.35 + val itms2fstr: I_Model.single -> string * string
9.36 + val par2fstr: I_Model.single -> string * TermC.as_string
9.37 + val parsitm: theory -> I_Model.single -> I_Model.single
9.38 + val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
9.39 + (''a * string) list ->
9.40 + (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
9.41 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.42 +end
9.43 +
9.44 +(**)
9.45 +structure P_Spec(**): PRESENTATION_SPECIFICATION(**) =
9.46 +struct
9.47 +(**)
9.48 +
9.49 +fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
9.50 +
9.51 +(** handle an input P_Specific'action **)
9.52 +
9.53 +datatype iitem =
9.54 + Given of TermC.as_string list
9.55 +(*Where is still not input*)
9.56 +| Find of TermC.as_string list
9.57 +| Relate of TermC.as_string list
9.58 +
9.59 +type imodel = iitem list
9.60 +
9.61 +type icalhd =
9.62 + Pos.pos' * (* the position in Ctree *)
9.63 + TermC.as_string * (* the headline shown on Calc.T *)
9.64 + imodel * (* the model *)
9.65 + Pos.pos_ * (* model belongs to Problem or Method *)
9.66 + References.T; (* into Know_Store *)
9.67 +val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
9.68 +
9.69 +(* re-parse itms with a new thy and prepare for checking with ori list *)
9.70 +fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
9.71 + (let val t = Input_Descript.join (d, ts)
9.72 + val _ = (UnparseC.term_in_thy dI t)
9.73 + (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
9.74 + in itm end
9.75 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
9.76 + | parsitm dI (i, v, b, f, I_Model.Syn str) =
9.77 + (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
9.78 + in (i, v, b ,f, I_Model.Par str) end
9.79 + handle _ => (i, v, b, f, I_Model.Syn str))
9.80 + | parsitm dI (i, v, b, f, I_Model.Typ str) =
9.81 + (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
9.82 + in (i, v, b, f, I_Model.Par str) end
9.83 + handle _ => (i, v, b, f, I_Model.Syn str))
9.84 + | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
9.85 + (let val t = Input_Descript.join (d,ts);
9.86 + val _ = UnparseC.term_in_thy dI t;
9.87 + (*this ^ should raise the exn on unability of re-parsing dts*)
9.88 + in itm end
9.89 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
9.90 + | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
9.91 + (let val t = Input_Descript.join (d,ts);
9.92 + val _ = UnparseC.term_in_thy dI t;
9.93 + (*this ^ should raise the exn on unability of re-parsing dts*)
9.94 + in itm end
9.95 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
9.96 + | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
9.97 + (let val t = d $ t';
9.98 + val _ = UnparseC.term_in_thy dI t;
9.99 + (*this ^ should raise the exn on unability of re-parsing dts*)
9.100 + in itm end
9.101 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
9.102 + | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
9.103 + raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
9.104 +
9.105 +(*separate a list to a pair of elements that do NOT satisfy the predicate,
9.106 + and of elements that satisfy the predicate, i.e. (false, true)*)
9.107 +fun filter_sep pred xs =
9.108 + let
9.109 + fun filt ab [] = ab
9.110 + | filt (a, b) (x :: xs) =
9.111 + if pred x
9.112 + then filt (a, b @ [x]) xs
9.113 + else filt (a @ [x], b) xs
9.114 + in filt ([], []) xs end;
9.115 +fun is_Par (_, _, _, _, I_Model.Par _) = true
9.116 + | is_Par _ = false;
9.117 +
9.118 +fun is_e_ts [] = true
9.119 + | is_e_ts [Const ("List.list.Nil", _)] = true
9.120 + | is_e_ts _ = false;
9.121 +
9.122 +(* WN.9.11.03 copied from fun appl_add *)
9.123 +fun appl_add' dI oris ppc pbt (sel, ct) =
9.124 + let
9.125 + val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
9.126 + in
9.127 + case TermC.parseNEW ctxt ct of
9.128 + NONE => (0, [], false, sel, I_Model.Syn ct)
9.129 + | SOME t =>
9.130 + (case I_Model.is_known ctxt sel oris t of
9.131 + ("", ori', all) =>
9.132 + (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
9.133 + ("",itm) => itm
9.134 + | (msg,_) => raise ERROR ("appl_add': " ^ msg))
9.135 + | (_, (i, v, _, d, ts), _) =>
9.136 + if is_e_ts ts
9.137 + then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
9.138 + else (i, v, false, sel, I_Model.Sup (d, ts)))
9.139 + end
9.140 +
9.141 +(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
9.142 +fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
9.143 +fun fstr2itm_ thy pbt (f, str) =
9.144 + let
9.145 + val topt = TermC.parse thy str
9.146 + in
9.147 + case topt of
9.148 + NONE => ([], false, f, I_Model.Syn str)
9.149 + | SOME ct =>
9.150 + let
9.151 + val (d, ts) = (Input_Descript.split o Thm.term_of) ct
9.152 + val popt = find_first (eq7 (f, d)) pbt
9.153 + in
9.154 + case popt of
9.155 + NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
9.156 + | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
9.157 + end
9.158 + end
9.159 +
9.160 +(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
9.161 +fun unknown_expl dI pbt selcts =
9.162 + let
9.163 + val thy = ThyC.get_theory dI
9.164 + val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
9.165 + val its = O_Model.add_id its_
9.166 + in map flattup2 its end
9.167 +
9.168 +(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
9.169 + appl_add': generate 1 item
9.170 + appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
9.171 + appl_add' . is_notyet_input: compare with items in model already input
9.172 + insert_ppc': insert this 1 item*)
9.173 +fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
9.174 + (*already present itms in model are being overwritten*)
9.175 + | appl_adds _ _ ppc _ [] = ppc
9.176 + | appl_adds dI oris ppc pbt (selct :: ss) =
9.177 + let val itm = appl_add' dI oris ppc pbt selct;
9.178 + in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
9.179 +
9.180 +fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
9.181 + | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
9.182 +fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
9.183 + | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
9.184 + | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
9.185 + | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
9.186 + | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
9.187 + | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
9.188 + | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
9.189 + raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
9.190 +
9.191 +fun imodel2fstr iitems =
9.192 + let
9.193 + fun xxx is [] = is
9.194 + | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
9.195 + | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
9.196 + | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
9.197 + in xxx [] iitems end;
9.198 +
9.199 +(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
9.200 +fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
9.201 + let
9.202 + val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
9.203 + Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
9.204 + spec = sspec as (sdI, spI, smI), probl, meth, ...}
9.205 + => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
9.206 + | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
9.207 + in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf))
9.208 + else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
9.209 + let val (pos_, pits, mits) =
9.210 + if dI <> sdI
9.211 + then let val its = map (parsitm (ThyC.get_theory dI)) probl;
9.212 + val (its, trms) = filter_sep is_Par its;
9.213 + val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec))
9.214 + in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
9.215 + else
9.216 + if pI <> spI
9.217 + then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
9.218 + else
9.219 + let val pbt = (#ppc o Problem.from_store) pI
9.220 + val dI' = #1 (References.select ospec spec)
9.221 + val oris = if pI = #2 ospec then oris
9.222 + else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
9.223 + in (Pos.Pbl, appl_adds dI' oris probl pbt
9.224 + (map itms2fstr probl), meth) end
9.225 + else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
9.226 + then let val met = (#ppc o Method.from_store) mI
9.227 + val mits = Specification.complete_metitms oris probl meth met
9.228 + in if foldl and_ (true, map #3 mits)
9.229 + then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
9.230 + end
9.231 + else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)]
9.232 + ((#ppc o Problem.from_store) (#2 (References.select ospec spec)))
9.233 + (imodel2fstr imodel), meth)
9.234 + val pt = Ctree.update_spec pt p spec;
9.235 + in if pos_ = Pos.Pbl
9.236 + then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
9.237 + val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
9.238 + in (Ctree.update_pbl pt p pits,
9.239 + (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
9.240 + end
9.241 + else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
9.242 + val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
9.243 + in (Ctree.update_met pt p mits,
9.244 + (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
9.245 + end
9.246 + end
9.247 + end
9.248 + | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
9.249 +
9.250 +(**)end (**)
9.251 \ No newline at end of file
10.1 --- a/src/Tools/isac/Specify/p-specific.sml Fri May 15 11:46:43 2020 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,247 +0,0 @@
10.4 -(* Title: Specify/input-calchead.sml
10.5 - Author: Walther Neuper
10.6 - (c) due to copyright terms
10.7 -
10.8 -This will be dropped at switch to Isabelle/PIDE.
10.9 -*)
10.10 -
10.11 -signature INPUT_SPECIFICATION =
10.12 -sig
10.13 - datatype iitem =
10.14 - Find of TermC.as_string list
10.15 - | Given of TermC.as_string list
10.16 - | Relate of TermC.as_string list
10.17 - type imodel = iitem list
10.18 - type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
10.19 - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
10.20 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.21 - (* NONE *)
10.22 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.23 - val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
10.24 - string * TermC.as_string -> I_Model.single
10.25 - val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
10.26 - (string * TermC.as_string) list -> I_Model.T
10.27 - val e_icalhd: icalhd
10.28 - val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
10.29 - val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
10.30 - val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
10.31 - int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
10.32 - val imodel2fstr: iitem list -> (string * TermC.as_string) list
10.33 - val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
10.34 - val is_e_ts: term list -> bool
10.35 - val itms2fstr: I_Model.single -> string * string
10.36 - val par2fstr: I_Model.single -> string * TermC.as_string
10.37 - val parsitm: theory -> I_Model.single -> I_Model.single
10.38 - val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
10.39 - (''a * string) list ->
10.40 - (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
10.41 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.42 -end
10.43 -
10.44 -(**)
10.45 -structure P_Specific(**): INPUT_SPECIFICATION(**) =
10.46 -struct
10.47 -(**)
10.48 -
10.49 -fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
10.50 -
10.51 -(** handle an input P_Specific'action **)
10.52 -
10.53 -datatype iitem =
10.54 - Given of TermC.as_string list
10.55 -(*Where is still not input*)
10.56 -| Find of TermC.as_string list
10.57 -| Relate of TermC.as_string list
10.58 -
10.59 -type imodel = iitem list
10.60 -
10.61 -type icalhd =
10.62 - Pos.pos' * (* the position in Ctree *)
10.63 - TermC.as_string * (* the headline shown on Calc.T *)
10.64 - imodel * (* the model *)
10.65 - Pos.pos_ * (* model belongs to Problem or Method *)
10.66 - References.T; (* into Know_Store *)
10.67 -val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
10.68 -
10.69 -(* re-parse itms with a new thy and prepare for checking with ori list *)
10.70 -fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
10.71 - (let val t = Input_Descript.join (d, ts)
10.72 - val _ = (UnparseC.term_in_thy dI t)
10.73 - (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
10.74 - in itm end
10.75 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
10.76 - | parsitm dI (i, v, b, f, I_Model.Syn str) =
10.77 - (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
10.78 - in (i, v, b ,f, I_Model.Par str) end
10.79 - handle _ => (i, v, b, f, I_Model.Syn str))
10.80 - | parsitm dI (i, v, b, f, I_Model.Typ str) =
10.81 - (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
10.82 - in (i, v, b, f, I_Model.Par str) end
10.83 - handle _ => (i, v, b, f, I_Model.Syn str))
10.84 - | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
10.85 - (let val t = Input_Descript.join (d,ts);
10.86 - val _ = UnparseC.term_in_thy dI t;
10.87 - (*this ^ should raise the exn on unability of re-parsing dts*)
10.88 - in itm end
10.89 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
10.90 - | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
10.91 - (let val t = Input_Descript.join (d,ts);
10.92 - val _ = UnparseC.term_in_thy dI t;
10.93 - (*this ^ should raise the exn on unability of re-parsing dts*)
10.94 - in itm end
10.95 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
10.96 - | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
10.97 - (let val t = d $ t';
10.98 - val _ = UnparseC.term_in_thy dI t;
10.99 - (*this ^ should raise the exn on unability of re-parsing dts*)
10.100 - in itm end
10.101 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
10.102 - | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
10.103 - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
10.104 -
10.105 -(*separate a list to a pair of elements that do NOT satisfy the predicate,
10.106 - and of elements that satisfy the predicate, i.e. (false, true)*)
10.107 -fun filter_sep pred xs =
10.108 - let
10.109 - fun filt ab [] = ab
10.110 - | filt (a, b) (x :: xs) =
10.111 - if pred x
10.112 - then filt (a, b @ [x]) xs
10.113 - else filt (a @ [x], b) xs
10.114 - in filt ([], []) xs end;
10.115 -fun is_Par (_, _, _, _, I_Model.Par _) = true
10.116 - | is_Par _ = false;
10.117 -
10.118 -fun is_e_ts [] = true
10.119 - | is_e_ts [Const ("List.list.Nil", _)] = true
10.120 - | is_e_ts _ = false;
10.121 -
10.122 -(* WN.9.11.03 copied from fun appl_add *)
10.123 -fun appl_add' dI oris ppc pbt (sel, ct) =
10.124 - let
10.125 - val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
10.126 - in
10.127 - case TermC.parseNEW ctxt ct of
10.128 - NONE => (0, [], false, sel, I_Model.Syn ct)
10.129 - | SOME t =>
10.130 - (case I_Model.is_known ctxt sel oris t of
10.131 - ("", ori', all) =>
10.132 - (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
10.133 - ("",itm) => itm
10.134 - | (msg,_) => raise ERROR ("appl_add': " ^ msg))
10.135 - | (_, (i, v, _, d, ts), _) =>
10.136 - if is_e_ts ts
10.137 - then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
10.138 - else (i, v, false, sel, I_Model.Sup (d, ts)))
10.139 - end
10.140 -
10.141 -(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
10.142 -fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
10.143 -fun fstr2itm_ thy pbt (f, str) =
10.144 - let
10.145 - val topt = TermC.parse thy str
10.146 - in
10.147 - case topt of
10.148 - NONE => ([], false, f, I_Model.Syn str)
10.149 - | SOME ct =>
10.150 - let
10.151 - val (d, ts) = (Input_Descript.split o Thm.term_of) ct
10.152 - val popt = find_first (eq7 (f, d)) pbt
10.153 - in
10.154 - case popt of
10.155 - NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
10.156 - | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
10.157 - end
10.158 - end
10.159 -
10.160 -(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
10.161 -fun unknown_expl dI pbt selcts =
10.162 - let
10.163 - val thy = ThyC.get_theory dI
10.164 - val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
10.165 - val its = O_Model.add_id its_
10.166 - in map flattup2 its end
10.167 -
10.168 -(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
10.169 - appl_add': generate 1 item
10.170 - appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
10.171 - appl_add' . is_notyet_input: compare with items in model already input
10.172 - insert_ppc': insert this 1 item*)
10.173 -fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
10.174 - (*already present itms in model are being overwritten*)
10.175 - | appl_adds _ _ ppc _ [] = ppc
10.176 - | appl_adds dI oris ppc pbt (selct :: ss) =
10.177 - let val itm = appl_add' dI oris ppc pbt selct;
10.178 - in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
10.179 -
10.180 -fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
10.181 - | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
10.182 -fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
10.183 - | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
10.184 - | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
10.185 - | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
10.186 - | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
10.187 - | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
10.188 - | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
10.189 - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
10.190 -
10.191 -fun imodel2fstr iitems =
10.192 - let
10.193 - fun xxx is [] = is
10.194 - | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
10.195 - | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
10.196 - | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
10.197 - in xxx [] iitems end;
10.198 -
10.199 -(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
10.200 -fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
10.201 - let
10.202 - val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
10.203 - Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
10.204 - spec = sspec as (sdI, spI, smI), probl, meth, ...}
10.205 - => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
10.206 - | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
10.207 - in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf))
10.208 - else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
10.209 - let val (pos_, pits, mits) =
10.210 - if dI <> sdI
10.211 - then let val its = map (parsitm (ThyC.get_theory dI)) probl;
10.212 - val (its, trms) = filter_sep is_Par its;
10.213 - val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec))
10.214 - in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
10.215 - else
10.216 - if pI <> spI
10.217 - then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
10.218 - else
10.219 - let val pbt = (#ppc o Problem.from_store) pI
10.220 - val dI' = #1 (References.select ospec spec)
10.221 - val oris = if pI = #2 ospec then oris
10.222 - else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
10.223 - in (Pos.Pbl, appl_adds dI' oris probl pbt
10.224 - (map itms2fstr probl), meth) end
10.225 - else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
10.226 - then let val met = (#ppc o Method.from_store) mI
10.227 - val mits = Specification.complete_metitms oris probl meth met
10.228 - in if foldl and_ (true, map #3 mits)
10.229 - then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
10.230 - end
10.231 - else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)]
10.232 - ((#ppc o Problem.from_store) (#2 (References.select ospec spec)))
10.233 - (imodel2fstr imodel), meth)
10.234 - val pt = Ctree.update_spec pt p spec;
10.235 - in if pos_ = Pos.Pbl
10.236 - then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
10.237 - val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
10.238 - in (Ctree.update_pbl pt p pits,
10.239 - (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
10.240 - end
10.241 - else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
10.242 - val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
10.243 - in (Ctree.update_met pt p mits,
10.244 - (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
10.245 - end
10.246 - end
10.247 - end
10.248 - | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
10.249 -
10.250 -(**)end (**)
10.251 \ No newline at end of file
11.1 --- a/src/Tools/isac/Specify/refine.sml Fri May 15 11:46:43 2020 +0200
11.2 +++ b/src/Tools/isac/Specify/refine.sml Fri May 15 14:22:05 2020 +0200
11.3 @@ -13,7 +13,7 @@
11.4 val refine_ori' : O_Model.T -> Problem.id -> Problem.id
11.5
11.6 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.7 - val refine : Formalise.model -> Problem.id -> Model.match list
11.8 + val refine : Formalise.model -> Problem.id -> M_Match.T list
11.9 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.10 (*NONE*)
11.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.12 @@ -132,11 +132,11 @@
11.13
11.14 (* refine a problem; construct pblRD while scanning *)
11.15 fun refin pblRD ori (Store.Node (pI, [py], [])) =
11.16 - if Model.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
11.17 + if M_Match.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
11.18 then SOME (pblRD @ [pI])
11.19 else NONE
11.20 | refin pblRD ori (Store.Node (pI, [py], pys)) =
11.21 - if Model.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
11.22 + if M_Match.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
11.23 then (case refins (pblRD @ [pI]) ori pys of
11.24 SOME pblRD' => SOME pblRD'
11.25 | NONE => SOME (pblRD @ [pI]))
11.26 @@ -155,11 +155,11 @@
11.27 val {thy, ppc, where_, prls, ...} = py
11.28 val oris = O_Model.init fmz thy ppc(* |> #1*);
11.29 (* WN020803: itms!: oris might _not_ be complete here *)
11.30 - val (b, (itms, pre')) = Model.match_oris' thy oris (ppc, where_, prls)
11.31 + val (b, (itms, pre')) = M_Match.match_oris' thy oris (ppc, where_, prls)
11.32 in
11.33 if b
11.34 - then pbls @ [Model.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
11.35 - else pbls @ [Model.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
11.36 + then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
11.37 + else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
11.38 end
11.39 | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
11.40 let
11.41 @@ -167,13 +167,13 @@
11.42 val {thy, ppc, where_, prls, ...} = py
11.43 val oris = O_Model.init fmz thy ppc(* |> #1*);
11.44 (* WN020803: itms!: oris might _not_ be complete here *)
11.45 - val(b, (itms, pre')) = Model.match_oris' thy oris (ppc,where_,prls);
11.46 + val(b, (itms, pre')) = M_Match.match_oris' thy oris (ppc,where_,prls);
11.47 in
11.48 if b
11.49 then
11.50 - let val pbl = Model.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
11.51 + let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
11.52 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
11.53 - else (pbls @ [Model.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
11.54 + else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
11.55 end
11.56 | refin' _ _ _ _ = raise ERROR "refin': uncovered fun def."
11.57 and refins' _ _ pbls [] = pbls
11.58 @@ -182,8 +182,8 @@
11.59 val pbls' = refin' pblRD fmz pbls p
11.60 in
11.61 case last_elem pbls' of
11.62 - Model.Matches _ => pbls'
11.63 - | Model.NoMatch _ => refins' pblRD fmz pbls' pts
11.64 + M_Match.Matches _ => pbls'
11.65 + | M_Match.NoMatch _ => refins' pblRD fmz pbls' pts
11.66 end;
11.67
11.68 (* apply a fun to a ptyps node *)
12.1 --- a/src/Tools/isac/Specify/specification.sml Fri May 15 11:46:43 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/specification.sml Fri May 15 14:22:05 2020 +0200
12.3 @@ -54,51 +54,69 @@
12.4 (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
12.5 add them to the model-pattern of met and let this input be done automatically;
12.6 respective items must be in fmz.
12.7 -#1# fmz contains items, which are stored in oris of the root(!)-problem.
12.8 - This allows to specify methods, which require more input as anticipated
12.9 - in writing partial_functions: such an item can be fetched from the root-problem's oris.
12.10 - A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically
12.11 - and thus is solved numerically.
12.12 -#2# TODO
12.13 *)
12.14 signature SPECIFICATION =
12.15 sig
12.16
12.17 type T = Specification_Def.T
12.18 - val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
12.19 - (string * (term * 'a)) list * (string * (term * 'b)) list -> References.T -> Pos.pos_ * Tactic.input
12.20
12.21 - val reset_calchead : Calc.T -> Calc.T
12.22 - val get_ocalhd : Calc.T -> T
12.23 - val ocalhd_complete : I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
12.24 - val all_modspec : Calc.T -> Calc.T
12.25 +(*val reset: Calc.T -> Calc.T*)
12.26 + val reset_calchead: Calc.T -> Calc.T
12.27 +(*val get: Calc.T -> T*)
12.28 + val get_ocalhd: Calc.T -> T
12.29 +(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
12.30 + val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
12.31 +(*val is_complete: Calc.T -> bool*)
12.32 + val is_complete_mod: Calc.T -> bool
12.33
12.34 - val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
12.35 - val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
12.36 +(*/------- to Specify from Specification -------\*)
12.37 +(*val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
12.38 + Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input*)
12.39 + val nxt_spec: Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
12.40 + Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input
12.41 +(*val do_all : Calc.T -> Calc.T*)
12.42 + val all_modspec: Calc.T -> Calc.T
12.43 +(*val finish_phase: Calc.T -> Calc.T*)
12.44 + val complete_mod: Calc.T -> Calc.T
12.45 +(*val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option*)
12.46 + val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option
12.47 +(*val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post*)
12.48 + val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post
12.49 +(*val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post*)
12.50 + val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
12.51 +(*\------- to Specify from Specification -------/*)
12.52
12.53 - val complete_mod : Calc.T -> Calc.T
12.54 - val is_complete_mod : Calc.T -> bool
12.55 - val complete_spec : Calc.T -> Calc.T
12.56 - val is_complete_spec : Calc.T -> bool
12.57 +(*/------- to References/\<rightarrow>Def from Specification -------\*)
12.58 +(*FIRST DO 1. References-> References_Def 2./Specify/references.sml*)
12.59 +(*val complete: Calc.T -> Calc.T*)
12.60 + val complete_spec: Calc.T -> Calc.T
12.61 +(*val are_complete: Calc.T -> bool*)
12.62 + val is_complete_spec: Calc.T -> bool
12.63 +(*\------- to References/\<rightarrow>Def from Specification -------/*)
12.64
12.65 - val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T
12.66 - val match_ags_msg : Problem.id -> term -> term list -> unit
12.67 - val oris2fmz_vals : O_Model.T -> string list * term list
12.68 - val vars_of_pbl_' : Model_Pattern.T -> term list
12.69 +(*/------- to O_Model from Specification -------\*)
12.70 + val match_ags: theory -> Model_Pattern.T -> term list -> O_Model.T
12.71 + val match_ags_msg: Problem.id -> term -> term list -> unit
12.72 + val oris2fmz_vals: O_Model.T -> string list * term list
12.73 + val vars_of_pbl_': Model_Pattern.T -> term list
12.74 +(*\------- to O_Model from Specification -------/*)
12.75
12.76 - val ppc2list : 'a P_Model.ppc -> 'a list
12.77 +(*/------- to I_Model from Specification -------\*)
12.78 + val complete_metitms: O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
12.79 + val insert_ppc': I_Model.single -> I_Model.T -> I_Model.T
12.80 + val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
12.81 + I_Model.T * I_Model.T
12.82 + val is_error: I_Model.feedback -> bool
12.83 + val itm_out: theory -> I_Model.feedback -> string
12.84 + val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool
12.85 +(*\------- to I_Model from Specification -------/*)
12.86
12.87 - val itm_out : theory -> I_Model.feedback -> string
12.88 +(*/------- to P_Model from Specification -------\*)
12.89 + val ppc2list: 'a P_Model.ppc -> 'a list
12.90 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
12.91 val mk_additem: string -> TermC.as_string -> Tactic.input
12.92 - val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option
12.93 - val is_error: I_Model.feedback -> bool
12.94 - val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
12.95 - I_Model.T * I_Model.T
12.96 - val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post
12.97 - val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
12.98 +(*\------- to P_Model from Specification -------/*)
12.99
12.100 - val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool
12.101 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.102 (*NONE*)
12.103 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.104 @@ -116,16 +134,16 @@
12.105 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.106
12.107 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
12.108 - val variants_in : term list -> int
12.109 - val is_untouched : I_Model.single -> bool
12.110 - val is_list_type : typ -> bool
12.111 - val parse_ok : I_Model.feedback list -> bool
12.112 - val all_dsc_in : I_Model.feedback list -> term list
12.113 - val chktyps : theory -> term list * term list -> term list (* only in old tests*)
12.114 - val is_complete_modspec : Calc.T -> bool
12.115 - val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
12.116 + val variants_in: term list -> int
12.117 + val is_untouched: I_Model.single -> bool
12.118 + val is_list_type: typ -> bool
12.119 + val parse_ok: I_Model.feedback list -> bool
12.120 + val all_dsc_in: I_Model.feedback list -> term list
12.121 + val chktyps: theory -> term list * term list -> term list (* only in old tests*)
12.122 + val is_complete_modspec: Calc.T -> bool
12.123 + val get_formress: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
12.124 (string * Pos.pos' * term) list
12.125 - val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
12.126 + val get_forms: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
12.127 (string * Pos.pos' * term) list
12.128 end
12.129
12.130 @@ -273,7 +291,11 @@
12.131 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
12.132 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
12.133
12.134 -(* determine the next step of specification;
12.135 +(*/------- to Specify from Specification -------\*)
12.136 +(*
12.137 + TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met
12.138 +
12.139 + determine the next step of specification;
12.140 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
12.141 eg. in rootpbl 'no_met':
12.142 args:
12.143 @@ -319,6 +341,7 @@
12.144 else if not preok then (Pos.Met, Tactic.Specify_Method mI)
12.145 else (Pos.Met, Tactic.Apply_Method mI)))
12.146 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
12.147 +(*\------- to Specify from Specification -------/*)
12.148
12.149 (* make oris from args of the stac SubProblem and from pbt.
12.150 can this formal argument (of a model-pattern) be omitted in the arg-list
12.151 @@ -694,13 +717,16 @@
12.152 | is_complete_mod (_, pos) =
12.153 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
12.154
12.155 -(* have (thy, pbl, met) _all_ been specified explicitly ? *)
12.156 +(* have (thy, pbl, met) _all_ been specified explicitly ? RENAME References *)
12.157 fun is_complete_spec (pt, pos as (p, _)) =
12.158 - if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p
12.159 - then raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos)
12.160 + if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p then
12.161 + raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos)
12.162 else
12.163 - let val (dI,pI,mI) = Ctree.get_obj Ctree.g_spec pt p
12.164 - in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end
12.165 + let
12.166 + val (dI, pI, mI) = Ctree.get_obj Ctree.g_spec pt p
12.167 + in (* vvv--- shift to References *)
12.168 + dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
12.169 + end;
12.170
12.171 (* complete empty items in specification from origin (pbl, met ev.refined);
12.172 assumes 'is_complete_mod' *)
13.1 --- a/src/Tools/isac/Specify/specify-step.sml Fri May 15 11:46:43 2020 +0200
13.2 +++ b/src/Tools/isac/Specify/specify-step.sml Fri May 15 14:22:05 2020 +0200
13.3 @@ -79,7 +79,7 @@
13.4 val {ppc, where_, prls, ...} = Problem.from_store pID;
13.5 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
13.6 then (false, (I_Model.init ppc, []))
13.7 - else Model.match_itms_oris thy itms (ppc, where_, prls) oris;
13.8 + else M_Match.match_itms_oris thy itms (ppc, where_, prls) oris;
13.9 in
13.10 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
13.11 end
14.1 --- a/src/Tools/isac/Specify/specify.sml Fri May 15 11:46:43 2020 +0200
14.2 +++ b/src/Tools/isac/Specify/specify.sml Fri May 15 14:22:05 2020 +0200
14.3 @@ -1,4 +1,4 @@
14.4 -signature SPECIFY_NEW =
14.5 +signature SPECIFY =
14.6 sig
14.7 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
14.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.9 @@ -9,13 +9,14 @@
14.10 end
14.11
14.12 (**)
14.13 -structure Specify(**): SPECIFY_NEW(**) =
14.14 +structure Specify(**): SPECIFY(**) =
14.15 struct
14.16 (**)
14.17 open Pos
14.18 open Ctree
14.19 open Specification
14.20
14.21 +
14.22 fun find_next_step (pt, (p, p_)) =
14.23 let
14.24 val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
15.1 --- a/src/Tools/isac/Specify/step-specify.sml Fri May 15 11:46:43 2020 +0200
15.2 +++ b/src/Tools/isac/Specify/step-specify.sml Fri May 15 14:22:05 2020 +0200
15.3 @@ -132,7 +132,7 @@
15.4 val pbl =
15.5 if pI' = Problem.id_empty andalso pI = Problem.id_empty
15.6 then (false, (I_Model.init ppc, []))
15.7 - else Model.match_itms_oris thy probl (ppc,where_,prls) oris
15.8 + else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris
15.9 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
15.10 val (c, pt) =
15.11 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
15.12 @@ -153,7 +153,7 @@
15.13 val thy = ThyC.get_theory dI
15.14 val oris = O_Model.add thy ppc oris
15.15 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
15.16 - val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris
15.17 + val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc,pre,prls ) oris
15.18 val itms = hack_until_review_Specify_2 mID itms
15.19 val (pos, c, _, pt) =
15.20 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
15.21 @@ -249,7 +249,7 @@
15.22 val thy = ThyC.get_theory dI
15.23 val oris = O_Model.add thy ppc oris
15.24 val met = if met = [] then pbl else met
15.25 - val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris
15.26 + val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc, pre, prls) oris
15.27 val itms = hack_until_review_Specify_1 mI' itms
15.28 val (pos, _, _, pt) =
15.29 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
16.1 --- a/src/Tools/isac/Specify/test-out.sml Fri May 15 11:46:43 2020 +0200
16.2 +++ b/src/Tools/isac/Specify/test-out.sml Fri May 15 14:22:05 2020 +0200
16.3 @@ -54,7 +54,7 @@
16.4 Error_ of string (*<--*)
16.5 | FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*)
16.6 | PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.T) (*<--*)
16.7 -| RefineKF of Model.match list (*<--*)
16.8 +| RefineKF of M_Match.T list (*<--*)
16.9 | RefinedKF of (Problem.id * ((I_Model.T) * (Pre_Conds.T))) (*<--*)
16.10
16.11 datatype mout =
17.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri May 15 11:46:43 2020 +0200
17.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri May 15 14:22:05 2020 +0200
17.3 @@ -266,7 +266,7 @@
17.4 text \<open>\noindent Check if the given equation matches the specification of this
17.5 equation type.\<close>
17.6 ML \<open>
17.7 - Model.match_pbl fmz (Problem.from_store ["univariate","equation"]);
17.8 + M_Match.match_pbl fmz (Problem.from_store ["univariate","equation"]);
17.9 \<close>
17.10
17.11 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
17.12 @@ -290,7 +290,7 @@
17.13 specification of this equation type.\<close>
17.14
17.15 ML \<open>
17.16 - Model.match_pbl fmz (Problem.from_store
17.17 + M_Match.match_pbl fmz (Problem.from_store
17.18 ["abcFormula","degree_2","polynomial","univariate","equation"]);
17.19 \<close>
17.20
18.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 15 11:46:43 2020 +0200
18.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 15 14:22:05 2020 +0200
18.3 @@ -894,8 +894,8 @@
18.4
18.5 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
18.6 "solve (x+1=2, x)",(*the headline*)
18.7 - [P_Specific.Given ["equality (x+1=(2::real))", "solveFor x"],
18.8 - P_Specific.Find ["solutions L"](*,P_Specific.Relate []*)],
18.9 + [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
18.10 + P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)],
18.11 Pbl,
18.12 ("Test",
18.13 ["sqroot-test","univariate","equation","test"],
18.14 @@ -961,9 +961,9 @@
18.15 val spec = ("DiffApp", ["maximum_of","function"],
18.16 ["DiffApp","max_by_calculus"]);
18.17 (*the empty model with descriptions for user-guidance by Model_Problem*)
18.18 - val empty_model = [P_Specific.Given ["fixedValues []"],
18.19 - P_Specific.Find ["maximum", "valuesFor"],
18.20 - P_Specific.Relate ["relations []"]];
18.21 + val empty_model = [P_Spec.Given ["fixedValues []"],
18.22 + P_Spec.Find ["maximum", "valuesFor"],
18.23 + P_Spec.Relate ["relations []"]];
18.24 DEconstrCalcTree 1;
18.25
18.26 "#################################################################";
18.27 @@ -985,9 +985,9 @@
18.28 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
18.29 "Problem (DiffApp.thy, [maximum_of, function])",
18.30 (*the head-form ^^^ is not used for input here*)
18.31 - [P_Specific.Given ["fixedValues [r=Arbfix]"(*new input*)],
18.32 - P_Specific.Find ["maximum b"(*new input*), "valuesFor"],
18.33 - P_Specific.Relate ["relations"]],
18.34 + [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
18.35 + P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
18.36 + P_Spec.Relate ["relations"]],
18.37 (*input (Arbfix will dissappear soon)*)
18.38 Pbl (*belongsto*),
18.39 References.empty (*no input to the specification*));
18.40 @@ -1001,30 +1001,30 @@
18.41
18.42 (*this input completes the model*)
18.43 modifyCalcHead 1 (([],Pbl), "not used here",
18.44 - [P_Specific.Given ["fixedValues [r=Arbfix]"],
18.45 - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.46 - P_Specific.Relate ["relations [A=a*b, \
18.47 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
18.48 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.49 + P_Spec.Relate ["relations [A=a*b, \
18.50 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, References.empty);
18.51
18.52 (*specification is not interesting and should be skipped by the dialogguide;
18.53 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
18.54 modifyCalcHead 1 (([],Pbl), "not used here",
18.55 - [P_Specific.Given ["fixedValues [r=Arbfix]"],
18.56 - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.57 - P_Specific.Relate ["relations [A=a*b, \
18.58 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
18.59 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.60 + P_Spec.Relate ["relations [A=a*b, \
18.61 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
18.62 ("DiffApp", ["empty_probl_id"], ["empty_meth_id"]));
18.63 modifyCalcHead 1 (([],Pbl), "not used here",
18.64 - [P_Specific.Given ["fixedValues [r=Arbfix]"],
18.65 - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.66 - P_Specific.Relate ["relations [A=a*b, \
18.67 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
18.68 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.69 + P_Spec.Relate ["relations [A=a*b, \
18.70 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
18.71 ("DiffApp", ["maximum_of","function"],
18.72 ["empty_meth_id"]));
18.73 modifyCalcHead 1 (([],Pbl), "not used here",
18.74 - [P_Specific.Given ["fixedValues [r=Arbfix]"],
18.75 - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.76 - P_Specific.Relate ["relations [A=a*b, \
18.77 + [P_Spec.Given ["fixedValues [r=Arbfix]"],
18.78 + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
18.79 + P_Spec.Relate ["relations [A=a*b, \
18.80 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
18.81 ("DiffApp", ["maximum_of","function"],
18.82 ["DiffApp","max_by_calculus"]));
18.83 @@ -1040,8 +1040,8 @@
18.84 Iterator 1; moveActiveRoot 1;
18.85 refFormula 1 (get_pos 1 1);
18.86 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
18.87 - [P_Specific.Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
18.88 - P_Specific.Find ["solutions L"]],
18.89 + [P_Spec.Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
18.90 + P_Spec.Find ["solutions L"]],
18.91 Pbl,
18.92 ("Test", ["LINEAR","univariate","equation","test"],
18.93 ["Test","solve_linear"]));
19.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Fri May 15 11:46:43 2020 +0200
19.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri May 15 14:22:05 2020 +0200
19.3 @@ -316,10 +316,10 @@
19.4 "===== case 1 =====";
19.5 val matches = Refine.refine fmz ["LINEAR","system"];
19.6 case matches of
19.7 - [Model.Matches (["LINEAR", "system"], _),
19.8 - Model.Matches (["2x2", "LINEAR", "system"], _),
19.9 - Model.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
19.10 - Model.Matches (["normalise", "2x2", "LINEAR", "system"],
19.11 + [M_Match.Matches (["LINEAR", "system"], _),
19.12 + M_Match.Matches (["2x2", "LINEAR", "system"], _),
19.13 + M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
19.14 + M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],
19.15 {Find = [Correct "solution LL"],
19.16 With = [],
19.17 Given =
19.18 @@ -335,7 +335,7 @@
19.19 "solveForVars [c, c_2]", "solution LL"];
19.20 val matches = Refine.refine fmz ["LINEAR","system"];
19.21 case matches of [_,_,
19.22 - Model.Matches
19.23 + M_Match.Matches
19.24 (["triangular", "2x2", "LINEAR", "system"],
19.25 {Find = [Correct "solution LL"],
19.26 With = [],
19.27 @@ -391,13 +391,13 @@
19.28 \-------------------------------------------------------/
19.29 val matches = Refine.refine fmz ["LINEAR","system"];
19.30 case matches of
19.31 - [Model.Matches (["LINEAR", "system"], _),
19.32 - Model.NoMatch (["2x2", "LINEAR", "system"], _),
19.33 - Model.NoMatch (["3x3", "LINEAR", "system"], _),
19.34 - Model.Matches (["4x4", "LINEAR", "system"], _),
19.35 - Model.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
19.36 - Model.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
19.37 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys Model.NoMatch";
19.38 + [M_Match.Matches (["LINEAR", "system"], _),
19.39 + M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
19.40 + M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
19.41 + M_Match.Matches (["4x4", "LINEAR", "system"], _),
19.42 + M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
19.43 + M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
19.44 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
19.45 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
19.46
19.47 "===== case 4 =====";
19.48 @@ -408,8 +408,8 @@
19.49 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
19.50 val matches = Refine.refine fmz ["triangular", "4x4", "LINEAR","system"];
19.51 case matches of
19.52 - [Model.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
19.53 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys Model.NoMatch";
19.54 + [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
19.55 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
19.56 val matches = Refine.refine fmz ["LINEAR","system"];
19.57 ============ inhibit exn WN120314 ==============================================*)
19.58
20.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri May 15 11:46:43 2020 +0200
20.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri May 15 14:22:05 2020 +0200
20.3 @@ -565,7 +565,7 @@
20.4 val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];
20.5 "-----0 ---";
20.6 case Refine.refine fmz ["polynomial","simplification"]of
20.7 - [Model.Matches (["polynomial", "simplification"], _)] => ()
20.8 + [M_Match.Matches (["polynomial", "simplification"], _)] => ()
20.9 | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
20.10 (*...if there is an error, then ...*)
20.11
20.12 @@ -574,12 +574,12 @@
20.13 val pbt = Problem.from_store ["polynomial","simplification"];
20.14 (*default_print_depth 3;*)
20.15 (*if there is ...
20.16 -> val Model.NoMatch' {Given=gi, Where=wh, Find=fi,...} = Model.match_pbl fmz pbt;
20.17 +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
20.18 ... then Rewrite.trace_on:*)
20.19
20.20 "-----2 ---";
20.21 Rewrite.trace_on := false;
20.22 -Model.match_pbl fmz pbt;
20.23 +M_Match.match_pbl fmz pbt;
20.24 Rewrite.trace_on := false;
20.25 (*... if there is no rewrite, then there is something wrong with prls*)
20.26
20.27 @@ -596,10 +596,10 @@
20.28 "-----4 ---";
20.29 (*show_types:=true;*)
20.30 (*
20.31 -> val Model.NoMatch' {Given=gi, Where=wh, Find=fi,...} = Model.match_pbl fmz pbt;
20.32 +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
20.33 val wh = [False "(t_::real => real) (is_polyexp::real)"]
20.34 ......................^^^^^^^^^^^^...............^^^^*)
20.35 -val Model.Matches' _ = Model.match_pbl fmz pbt;
20.36 +val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
20.37 (*show_types:=false;*)
20.38
20.39
21.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Fri May 15 11:46:43 2020 +0200
21.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Fri May 15 14:22:05 2020 +0200
21.3 @@ -109,22 +109,22 @@
21.4 "----------- test matching problems --------------------------0---";
21.5 "----------- test matching problems --------------------------0---";
21.6 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
21.7 -if Model.match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) =
21.8 - Model.Matches' {Find = [Correct "solutions L"],
21.9 +if M_Match.match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) =
21.10 + M_Match.Matches' {Find = [Correct "solutions L"],
21.11 With = [],
21.12 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
21.13 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
21.14 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
21.15 Relate = []}
21.16 -then () else error "Model.match_pbl [expanded,univariate,equation]";
21.17 +then () else error "M_Match.match_pbl [expanded,univariate,equation]";
21.18
21.19 -if Model.match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) =
21.20 - Model.Matches' {Find = [Correct "solutions L"],
21.21 +if M_Match.match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) =
21.22 + M_Match.Matches' {Find = [Correct "solutions L"],
21.23 With = [],
21.24 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
21.25 Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
21.26 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
21.27 -then () else error "Model.match_pbl [degree_2,expanded,univariate,equation]";
21.28 +then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
21.29
21.30
21.31 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
22.1 --- a/test/Tools/isac/Knowledge/rateq.sml Fri May 15 11:46:43 2020 +0200
22.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri May 15 14:22:05 2020 +0200
22.3 @@ -40,13 +40,13 @@
22.4 val result = UnparseC.term t_;
22.5 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
22.6
22.7 -val result = Model.match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
22.8 +val result = M_Match.match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
22.9 (Problem.from_store ["rational","univariate","equation"]);
22.10 -case result of Model.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
22.11 +case result of M_Match.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
22.12
22.13 -val result = Model.match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
22.14 +val result = M_Match.match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
22.15 (Problem.from_store ["rational","univariate","equation"]);
22.16 -case result of Model.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
22.17 +case result of M_Match.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
22.18
22.19 "------------ solve (1/x = 5, x) by me ---------------------------";
22.20 "------------ solve (1/x = 5, x) by me ---------------------------";
23.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Fri May 15 11:46:43 2020 +0200
23.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Fri May 15 14:22:05 2020 +0200
23.3 @@ -84,13 +84,13 @@
23.4
23.5
23.6
23.7 -val result = Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
23.8 +val result = M_Match.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
23.9 (Problem.from_store ["rootX","univariate","equation"]);
23.10 -case result of Model.Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
23.11 +case result of M_Match.Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
23.12
23.13 -val result = Model.match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
23.14 +val result = M_Match.match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
23.15 (Problem.from_store ["rootX","univariate","equation"]);
23.16 -case result of Model.NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
23.17 +case result of M_Match.NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
23.18
23.19 (*---------rooteq---- 23.8.02 ---------------------*)
23.20 "---------(1/sqrt(x)=5)---------------------";
23.21 @@ -778,6 +778,6 @@
23.22
23.23
23.24 Refine.refine fmz ["univariate","equation","test"];
23.25 -Model.match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]);
23.26 +M_Match.match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]);
23.27
23.28 ===== copied here from OLDTESTS in case there is a Program ===^^^=============================*)
24.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Fri May 15 11:46:43 2020 +0200
24.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Fri May 15 14:22:05 2020 +0200
24.3 @@ -65,7 +65,7 @@
24.4 [("Test","methode")])]
24.5 thy;
24.6
24.7 -Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);
24.8 +M_Match.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);
24.9
24.10 KEStore_Elems.add_pbts
24.11 [Problem.prep_input (theory "Isac_Knowledge")
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/test/Tools/isac/Specify/m-match.sml Fri May 15 14:22:05 2020 +0200
25.3 @@ -0,0 +1,17 @@
25.4 +(* Title: "Specify/model.sml"
25.5 + Author: Walther Neuper
25.6 + (c) due to copyright terms
25.7 +*)
25.8 +
25.9 +"-----------------------------------------------------------------------------------------------";
25.10 +"table of contents -----------------------------------------------------------------------------";
25.11 +"-----------------------------------------------------------------------------------------------";
25.12 +"----------- TODO ------------------------------------------------------------------------------";
25.13 +"-----------------------------------------------------------------------------------------------";
25.14 +"-----------------------------------------------------------------------------------------------";
25.15 +"-----------------------------------------------------------------------------------------------";
25.16 +
25.17 +open M_Match;
25.18 +"----------- TODO ------------------------------------------------------------------------------";
25.19 +"----------- TODO ------------------------------------------------------------------------------";
25.20 +"----------- TODO ------------------------------------------------------------------------------";
26.1 --- a/test/Tools/isac/Specify/model.sml Fri May 15 11:46:43 2020 +0200
26.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
26.3 @@ -1,17 +0,0 @@
26.4 -(* Title: "Specify/model.sml"
26.5 - Author: Walther Neuper
26.6 - (c) due to copyright terms
26.7 -*)
26.8 -
26.9 -"-----------------------------------------------------------------------------------------------";
26.10 -"table of contents -----------------------------------------------------------------------------";
26.11 -"-----------------------------------------------------------------------------------------------";
26.12 -"----------- TODO ------------------------------------------------------------------------------";
26.13 -"-----------------------------------------------------------------------------------------------";
26.14 -"-----------------------------------------------------------------------------------------------";
26.15 -"-----------------------------------------------------------------------------------------------";
26.16 -
26.17 -open Model;
26.18 -"----------- TODO ------------------------------------------------------------------------------";
26.19 -"----------- TODO ------------------------------------------------------------------------------";
26.20 -"----------- TODO ------------------------------------------------------------------------------";
27.1 --- a/test/Tools/isac/Specify/ptyps.sml Fri May 15 11:46:43 2020 +0200
27.2 +++ b/test/Tools/isac/Specify/ptyps.sml Fri May 15 14:22:05 2020 +0200
27.3 @@ -138,7 +138,7 @@
27.4 "solveFor x","errorBound (eps=0)","solutions L"];
27.5 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
27.6 Problem.from_store ["univariate","equation"];
27.7 -Model.match_pbl fmz pbt;
27.8 +M_Match.match_pbl fmz pbt;
27.9 *)
27.10 "----------- fun match_oris --------------------------------------";
27.11 "----------- fun match_oris --------------------------------------";
28.1 --- a/test/Tools/isac/Specify/refine.sml Fri May 15 11:46:43 2020 +0200
28.2 +++ b/test/Tools/isac/Specify/refine.sml Fri May 15 14:22:05 2020 +0200
28.3 @@ -116,10 +116,10 @@
28.4
28.5 (*case 1: no refinement *)
28.6 case Refine.refine fmz1 ["pbla", "refine", "test"] of
28.7 - [Model.Matches (["pbla", "refine", "test"], _),
28.8 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.9 - Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),
28.10 - Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
28.11 + [M_Match.Matches (["pbla", "refine", "test"], _),
28.12 + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.13 + M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),
28.14 + M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
28.15 | _ => error "--- Refine.refine test-pbtyps --- broken with case 1";
28.16 (*
28.17 *** pass ["pbla"]
28.18 @@ -127,22 +127,22 @@
28.19 *** pass ["pbla","pbla2"]
28.20 *** pass ["pbla","pbla3"]
28.21 val it =
28.22 - [Model.Matches
28.23 + [M_Match.Matches
28.24 (["pbla"],
28.25 {Find=[],
28.26 Given=[Correct "fixedValues [aaa = #0]",
28.27 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
28.28 - Model.NoMatch
28.29 + M_Match.NoMatch
28.30 (["pbla1","pbla"],
28.31 {Find=[],
28.32 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
28.33 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
28.34 - Model.NoMatch
28.35 + M_Match.NoMatch
28.36 (["pbla2","pbla"],
28.37 {Find=[],
28.38 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
28.39 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
28.40 - Model.NoMatch
28.41 + M_Match.NoMatch
28.42 (["pbla3","pbla"],
28.43 {Find=[],
28.44 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
28.45 @@ -151,10 +151,10 @@
28.46
28.47 (*case 2: refined to pbt without children *)
28.48 case Refine.refine fmz2 ["pbla", "refine", "test"] of
28.49 - [Model.Matches (["pbla", "refine", "test"], _),
28.50 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.51 - Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),
28.52 - Model.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
28.53 + [M_Match.Matches (["pbla", "refine", "test"], _),
28.54 + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.55 + M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),
28.56 + M_Match.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
28.57 | _ => error "--- Refine.refine test-pbtyps --- broken with case 2";
28.58 (*
28.59 *** pass ["pbla"]
28.60 @@ -162,22 +162,22 @@
28.61 *** pass ["pbla","pbla2"]
28.62 *** pass ["pbla","pbla3"]
28.63 val it =
28.64 - [Model.Matches
28.65 + [M_Match.Matches
28.66 (["pbla"],
28.67 {Find=[],
28.68 Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
28.69 Relate=[],Where=[],With=[]}),
28.70 - Model.NoMatch
28.71 + M_Match.NoMatch
28.72 (["pbla1","pbla"],
28.73 {Find=[],
28.74 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
28.75 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
28.76 - Model.NoMatch
28.77 + M_Match.NoMatch
28.78 (["pbla2","pbla"],
28.79 {Find=[],
28.80 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
28.81 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
28.82 - Model.Matches
28.83 + M_Match.Matches
28.84 (["pbla3","pbla"],
28.85 {Find=[],
28.86 Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
28.87 @@ -185,13 +185,13 @@
28.88
28.89 (*case 3: refined to pbt with children *)
28.90 case Refine.refine fmz3 ["pbla", "refine", "test"] of
28.91 - [Model.Matches (["pbla", "refine", "test"], _),
28.92 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.93 - Model.Matches (["pbla2", "pbla", "refine", "test"], _),
28.94 - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
28.95 - Model.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
28.96 - Model.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
28.97 - Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
28.98 + [M_Match.Matches (["pbla", "refine", "test"], _),
28.99 + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.100 + M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
28.101 + M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
28.102 + M_Match.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
28.103 + M_Match.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
28.104 + M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
28.105 | _ => error "--- Refine.refine test-pbtyps --- broken with case 3";
28.106 (*
28.107 *** pass ["pbla"]
28.108 @@ -202,37 +202,37 @@
28.109 *** pass ["pbla","pbla2","pbla2z"]
28.110 *** pass ["pbla","pbla3"]
28.111 val it =
28.112 - [Model.Matches
28.113 + [M_Match.Matches
28.114 (["pbla"],
28.115 {Find=[],
28.116 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
28.117 Relate=[],Where=[],With=[]}),
28.118 - Model.NoMatch
28.119 + M_Match.NoMatch
28.120 (["pbla1","pbla"],
28.121 {Find=[],
28.122 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
28.123 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
28.124 - Model.Matches
28.125 + M_Match.Matches
28.126 (["pbla2","pbla"],
28.127 {Find=[],
28.128 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
28.129 Relate=[],Where=[],With=[]}),
28.130 - Model.NoMatch
28.131 + M_Match.NoMatch
28.132 (["pbla2x","pbla2","pbla"],
28.133 {Find=[],
28.134 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.135 Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
28.136 - Model.NoMatch
28.137 + M_Match.NoMatch
28.138 (["pbla2y","pbla2","pbla"],
28.139 {Find=[],
28.140 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.141 Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
28.142 - Model.NoMatch
28.143 + M_Match.NoMatch
28.144 (["pbla2z","pbla2","pbla"],
28.145 {Find=[],
28.146 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.147 Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
28.148 - Model.NoMatch
28.149 + M_Match.NoMatch
28.150 (["pbla3","pbla"],
28.151 {Find=[],
28.152 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
28.153 @@ -241,11 +241,11 @@
28.154
28.155 (*case 4: refined to children (without child)*)
28.156 case Refine.refine fmz4 ["pbla", "refine", "test"] of
28.157 - [Model.Matches (["pbla", "refine", "test"], _),
28.158 - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.159 - Model.Matches (["pbla2", "pbla", "refine", "test"], _),
28.160 - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
28.161 - Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
28.162 + [M_Match.Matches (["pbla", "refine", "test"], _),
28.163 + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
28.164 + M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
28.165 + M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
28.166 + M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
28.167 | _ => error "--- Refine.refine test-pbtyps --- broken with case 4";
28.168 (*
28.169 *** pass ["pbla"]
28.170 @@ -254,29 +254,29 @@
28.171 *** pass ["pbla","pbla2","pbla2x"]
28.172 *** pass ["pbla","pbla2","pbla2y"]
28.173 val it =
28.174 - [Model.Matches
28.175 + [M_Match.Matches
28.176 (["pbla"],
28.177 {Find=[],
28.178 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
28.179 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
28.180 - Model.NoMatch
28.181 + M_Match.NoMatch
28.182 (["pbla1","pbla"],
28.183 {Find=[],
28.184 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
28.185 Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
28.186 Relate=[],Where=[],With=[]}),
28.187 - Model.Matches
28.188 + M_Match.Matches
28.189 (["pbla2","pbla"],
28.190 {Find=[],
28.191 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.192 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
28.193 - Model.NoMatch
28.194 + M_Match.NoMatch
28.195 (["pbla2x","pbla2","pbla"],
28.196 {Find=[],
28.197 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.198 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
28.199 Relate=[],Where=[],With=[]}),
28.200 - Model.Matches
28.201 + M_Match.Matches
28.202 (["pbla2y","pbla2","pbla"],
28.203 {Find=[],
28.204 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.205 @@ -285,27 +285,27 @@
28.206
28.207 (*case 5: start refinement somewhere in ptyps*)
28.208 case Refine.refine fmz4 ["pbla2","pbla", "refine", "test"] of
28.209 - [Model.Matches (["pbla2", "pbla", "refine", "test"], _),
28.210 - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
28.211 - Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
28.212 + [M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
28.213 + M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
28.214 + M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
28.215 | _ => error "--- Refine.refine test-pbtyps --- broken with case 5";
28.216 (*
28.217 *** pass ["pbla","pbla2"]
28.218 *** pass ["pbla","pbla2","pbla2x"]
28.219 *** pass ["pbla","pbla2","pbla2y"]
28.220 val it =
28.221 - [Model.Matches
28.222 + [M_Match.Matches
28.223 (["pbla2","pbla"],
28.224 {Find=[],
28.225 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.226 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
28.227 - Model.NoMatch
28.228 + M_Match.NoMatch
28.229 (["pbla2x","pbla2","pbla"],
28.230 {Find=[],
28.231 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
28.232 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
28.233 Relate=[],Where=[],With=[]}),
28.234 - Model.Matches
28.235 + M_Match.Matches
28.236 (["pbla2y","pbla2","pbla"],
28.237 {Find=[],
28.238 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",