# HG changeset patch # User Walther Neuper # Date 1589545325 -7200 # Node ID 08296690e7a6e063b270d7219b6c0fe6f7a5304c # Parent f1fdb213717b89ec2e5b11681cbde00af1481757 prep. cleanup of Specification diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/BridgeLibisabelle/datatypes.sml --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri May 15 14:22:05 2020 +0200 @@ -424,9 +424,9 @@ (*XML.Elem (("WHERE", []), wheres), ... Where is never input*) XML.Elem (("FIND", []), finds), XML.Elem (("RELATE", []), relates)])) = - ([P_Specific.Given (map xml_to_cterm givens), - P_Specific.Find (map xml_to_cterm finds), - P_Specific.Relate (map xml_to_cterm relates)]) : P_Specific.imodel + ([P_Spec.Given (map xml_to_cterm givens), + P_Spec.Find (map xml_to_cterm finds), + P_Spec.Relate (map xml_to_cterm relates)]) : P_Spec.imodel | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x) fun xml_to_icalhd (XML.Elem (( "ICALCHEAD", []), [ @@ -436,7 +436,7 @@ XML.Elem (( "POS", []), [XML.Text belongsto]), spec as XML.Elem (( "SPECIFICATION", []), _)])) = (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel, - Pos.str2pos_ belongsto, xml_to_spec spec) : P_Specific.icalhd + Pos.str2pos_ belongsto, xml_to_spec spec) : P_Spec.icalhd | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x) fun xml_of_sub (id, value) = diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/BridgeLibisabelle/interface.sml --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Fri May 15 14:22:05 2020 +0200 @@ -31,7 +31,7 @@ val Iterator : calcID -> XML.tree val IteratorTEST : calcID -> iterID val modelProblem : calcID -> XML.tree - val modifyCalcHead : calcID -> P_Specific.icalhd -> XML.tree + val modifyCalcHead : calcID -> P_Spec.icalhd -> XML.tree val moveActiveCalcHead : calcID -> XML.tree val moveActiveDown : calcID -> XML.tree val moveActiveFormula : calcID -> Pos.pos' -> XML.tree @@ -73,12 +73,12 @@ called for each cterm', icalhd, fmz in this interface; + see "fun en/decode" in /mathml.sml *) fun encode_imodel imodel = - let fun enc (P_Specific.Given ifos) = P_Specific.Given (map encode ifos) - | enc (P_Specific.Find ifos) = P_Specific.Find (map encode ifos) - | enc (P_Specific.Relate ifos) = P_Specific.Relate (map encode ifos) - in map enc imodel:P_Specific.imodel end; -fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Specific.icalhd) = - (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Specific.icalhd; + let fun enc (P_Spec.Given ifos) = P_Spec.Given (map encode ifos) + | enc (P_Spec.Find ifos) = P_Spec.Find (map encode ifos) + | enc (P_Spec.Relate ifos) = P_Spec.Relate (map encode ifos) + in map enc imodel:P_Spec.imodel end; +fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Spec.icalhd) = + (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Spec.icalhd; fun encode_fmz (ifos, spec) = (map encode ifos, spec); @@ -288,10 +288,10 @@ end) handle _ => sysERROR2xml cI "error in kernel 8"; -fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Specific.icalhd) = +fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) = (let val ((pt,_),_) = get_calc cI - val (pt, chd as (_,p_,_,_,_,_)) = P_Specific.input_icalhd pt ichd + val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end) handle _ => sysERROR2xml cI "error in kernel 9"; diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/MathEngine/mathengine-stateless.sml --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 15 14:22:05 2020 +0200 @@ -148,7 +148,7 @@ then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) else pI' val {ppc, where_, prls, ...} = Problem.from_store pblID - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os in (model_ok, pblID, hdl, pbl, pre) end @@ -163,7 +163,7 @@ then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) else mI' val {ppc, pre, prls, scr, ...} = Method.from_store metID - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os in (model_ok, metID, scr, pbl, pre) end @@ -176,7 +176,7 @@ Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl) | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case" val {ppc,where_,prls,...} = Problem.from_store pI - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os in (model_ok, pI, hdl, pbl, pre) end @@ -188,7 +188,7 @@ Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os) | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case" val {ppc,pre,prls,scr,...} = Method.from_store mI - val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os in (model_ok, mI, scr, pbl, pre) end @@ -204,7 +204,7 @@ NONE => (*copy from context_pbl*) let val {ppc,where_,prls,...} = Problem.from_store pI - val (_, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os + val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os in (false, pI, hdl, pbl, pre) end diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/Specify.thy --- a/src/Tools/isac/Specify/Specify.thy Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/Specify.thy Fri May 15 14:22:05 2020 +0200 @@ -12,13 +12,13 @@ ML_file "i-model.sml" ML_file "pre-conditions.sml" ML_file "p-model.sml" - ML_file model.sml + ML_file "m-match.sml" ML_file refine.sml ML_file "test-out.sml" ML_file "specify-step.sml" ML_file specification.sml ML_file "cas-command.sml" - ML_file "p-specific.sml" + ML_file "p-spec.sml" ML_file specify.sml ML_file "step-specify.sml" diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/formalise.sml --- a/src/Tools/isac/Specify/formalise.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/formalise.sml Fri May 15 14:22:05 2020 +0200 @@ -1,6 +1,11 @@ -(* Title: MathEngBasic/calc-tree-elem.sml +(* Title: Specify/formalise.sml Author: Walther Neuper 191026 (c) due to copyright terms + +A formalisation contains all data requred to solve a calculation. +Specifically in the root of a calculation the formalisation might contain items, +which are required by Subproblem's (e.g. "errorBound" in case an equation +cannot be solved symbolically and thus is solved numerically) *) signature FORMALISE = sig diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/m-match.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Specify/m-match.sml Fri May 15 14:22:05 2020 +0200 @@ -0,0 +1,143 @@ +(* Title: Specify/model.sml + Author: Walther Neuper 110226 + (c) due to copyright terms + +Operations on models. +*) + +signature MODEL_MATCH = +sig + datatype T = + Matches of Problem.id * P_Model.T + | NoMatch of Problem.id * P_Model.T + val matchs2str : T list -> string + + val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool +(*unify ^^^^^^^^^^ vvvvvvvvvv + vvvvvvvvv ^^^^^^^^^*) + val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> + bool * (I_Model.T * Pre_Conds.T) + val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> + O_Model.T -> bool * (I_Model.T * Pre_Conds.T) + +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) + datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T + val match_pbl : Formalise.model -> Problem.T -> match' +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) + (*NONE*) +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) +end + +(**) +structure M_Match(**) : MODEL_MATCH(**) = +struct +(**) + +datatype T = + Matches of Problem.id * P_Model.T +| NoMatch of Problem.id * P_Model.T; +fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")" + | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"; +fun matchs2str ms = (strs2str o (map match2str)) ms; + + +fun field_eq f (_, _, f', _, _) = f = f'; + +fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d'; +fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_; +fun eq1 d (_, (d', _)) = (d = d'); + +fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts)); + +(* check an ori for matching a problemtype by description; + returns true only for itms found in pbt *) +fun chk1_ (_: theory) pbt (i, vats, f, d, vs) = + case find_first (eq1 d) pbt of + SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))] + | NONE => []; + +(* elem 'p' of pbt contained in itms ? *) +fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false; +fun chk1_m' oris (p as (f, (d, t))) = + case find_first (eq2' p) oris of + SOME _ => [] + | NONE => [(f, I_Model.Mis (d, t))]; +fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_); + +fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc); +fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc); + +(* check a problem (ie. ori list) for matching a problemtype, + takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *) +fun match_oris thy prls oris (pbt,pre) = + let + val itms = (flat o (map (chk1_ thy pbt))) oris; + val mvat = I_Model.vars_of itms; + val complete = chk1_mis mvat itms pbt; + val pre' = Pre_Conds.check prls pre itms mvat; + val pb = foldl and_ (true, map fst pre'); + in if complete andalso pb then true else false end; + +(* check a problem (ie. ori list) for matching a problemtype, + returns items for output to math-experts *) +fun match_oris' thy oris (ppc, pre, prls) = + let + val itms = (flat o (map (chk1_ thy ppc))) oris; + val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris; + val mvat = I_Model.vars_of itms; + val miss = chk1_mis' oris ppc; + val pre' = Pre_Conds.check prls pre itms mvat; + val pb = foldl and_ (true, map fst pre'); + in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; + + +(** check a problem (ie. itm list) for matching a problemtype **) + +(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt, + for missing items get data from formalization (ie. ori list); + takes the I_Model.vars_of for concluding completeness (could be another!) + + (0) determine the most frequent variant mv in pbl + ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => + (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; + (3) newitms = filter (mv mem vat(news)) news + (4) pbt @ newitms *) +fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris = + let + (*0*)val mv = I_Model.max_vt pbl; + + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_; + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of + SOME _ => false | NONE => true; + (*1*)val mis = (filter (notmem pbl)) pbt; + + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d'; + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid)); + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; + val news = (flat o (map (oris2itms oris))) mis; + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv; + val newitms = filter mem_vat news; + (*4*)val itms' = pbl @ newitms; + val pre' = Pre_Conds.check prls pre itms' mv; + val pb = foldl and_ (true, map fst pre'); + in (length mis = 0 andalso pb, (itms', pre')) end; + + +(** for use by math-authors **) + +datatype match' = (* for the user *) + Matches' of P_Model.T +| NoMatch' of P_Model.T; + +(* match a formalization with a problem type, for tests *) +fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) = + let + val oris = O_Model.init fmz thy ppc(* |> #1*); + val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er); + in + if bool + then Matches' (P_Model.from thy itms pre') + else NoMatch' (P_Model.from thy itms pre') + end; + +(**)end(**) diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/model.sml --- a/src/Tools/isac/Specify/model.sml Fri May 15 11:46:43 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,143 +0,0 @@ -(* Title: Specify/model.sml - Author: Walther Neuper 110226 - (c) due to copyright terms - -Operations on models. -*) - -signature MODEL = -sig - datatype match = - Matches of Problem.id * P_Model.T - | NoMatch of Problem.id * P_Model.T - val matchs2str : match list -> string - - val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool -(*unify ^^^^^^^^^^ vvvvvvvvvv - vvvvvvvvv ^^^^^^^^^*) - val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> - bool * (I_Model.T * Pre_Conds.T) - val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> - O_Model.T -> bool * (I_Model.T * Pre_Conds.T) - -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) - datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T - val match_pbl : Formalise.model -> Problem.T -> match' -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - (*NONE*) -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) -end - -(**) -structure Model(** ) : MODEL( **) = -struct -(**) - -datatype match = - Matches of Problem.id * P_Model.T -| NoMatch of Problem.id * P_Model.T; -fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")" - | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"; -fun matchs2str ms = (strs2str o (map match2str)) ms; - - -fun field_eq f (_, _, f', _, _) = f = f'; - -fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d'; -fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_; -fun eq1 d (_, (d', _)) = (d = d'); - -fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts)); - -(* check an ori for matching a problemtype by description; - returns true only for itms found in pbt *) -fun chk1_ (_: theory) pbt (i, vats, f, d, vs) = - case find_first (eq1 d) pbt of - SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))] - | NONE => []; - -(* elem 'p' of pbt contained in itms ? *) -fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false; -fun chk1_m' oris (p as (f, (d, t))) = - case find_first (eq2' p) oris of - SOME _ => [] - | NONE => [(f, I_Model.Mis (d, t))]; -fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_); - -fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc); -fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc); - -(* check a problem (ie. ori list) for matching a problemtype, - takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *) -fun match_oris thy prls oris (pbt,pre) = - let - val itms = (flat o (map (chk1_ thy pbt))) oris; - val mvat = I_Model.vars_of itms; - val complete = chk1_mis mvat itms pbt; - val pre' = Pre_Conds.check prls pre itms mvat; - val pb = foldl and_ (true, map fst pre'); - in if complete andalso pb then true else false end; - -(* check a problem (ie. ori list) for matching a problemtype, - returns items for output to math-experts *) -fun match_oris' thy oris (ppc, pre, prls) = - let - val itms = (flat o (map (chk1_ thy ppc))) oris; - val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris; - val mvat = I_Model.vars_of itms; - val miss = chk1_mis' oris ppc; - val pre' = Pre_Conds.check prls pre itms mvat; - val pb = foldl and_ (true, map fst pre'); - in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; - - -(** check a problem (ie. itm list) for matching a problemtype **) - -(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt, - for missing items get data from formalization (ie. ori list); - takes the I_Model.vars_of for concluding completeness (could be another!) - - (0) determine the most frequent variant mv in pbl - ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => - (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; - (3) newitms = filter (mv mem vat(news)) news - (4) pbt @ newitms *) -fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris = - let - (*0*)val mv = I_Model.max_vt pbl; - - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_; - fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of - SOME _ => false | NONE => true; - (*1*)val mis = (filter (notmem pbl)) pbt; - - fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d'; - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid)); - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; - val news = (flat o (map (oris2itms oris))) mis; - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv; - val newitms = filter mem_vat news; - (*4*)val itms' = pbl @ newitms; - val pre' = Pre_Conds.check prls pre itms' mv; - val pb = foldl and_ (true, map fst pre'); - in (length mis = 0 andalso pb, (itms', pre')) end; - - -(** for use by math-authors **) - -datatype match' = (* for the user *) - Matches' of P_Model.T -| NoMatch' of P_Model.T; - -(* match a formalization with a problem type, for tests *) -fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) = - let - val oris = O_Model.init fmz thy ppc(* |> #1*); - val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er); - in - if bool - then Matches' (P_Model.from thy itms pre') - else NoMatch' (P_Model.from thy itms pre') - end; - -(**)end(**) diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/o-model.sml --- a/src/Tools/isac/Specify/o-model.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/o-model.sml Fri May 15 14:22:05 2020 +0200 @@ -2,7 +2,7 @@ Author: Walther Neuper 110226 (c) due to copyright terms -Original model created initially from Formale.T and Model_Pattern.T; +An original model is created initially from Formalise.T and Model_Pattern.T; This model makes student's editing via I_Model.T more efficient. TODO: revise with an example with more than 1 variant. *) diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/p-spec.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Specify/p-spec.sml Fri May 15 14:22:05 2020 +0200 @@ -0,0 +1,247 @@ +(* Title: Specify/input-calchead.sml + Author: Walther Neuper + (c) due to copyright terms + +This will be dropped at switch to Isabelle/PIDE. +*) + +signature PRESENTATION_SPECIFICATION = +sig + datatype iitem = + Find of TermC.as_string list + | Given of TermC.as_string list + | Relate of TermC.as_string list + type imodel = iitem list + type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) + (* NONE *) +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) + val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T -> + string * TermC.as_string -> I_Model.single + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T -> + (string * TermC.as_string) list -> I_Model.T + val e_icalhd: icalhd + val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool + val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list + val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string -> + int list * bool * ''a * I_Model.feedback (*I_Model.single'*) + val imodel2fstr: iitem list -> (string * TermC.as_string) list + val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*) + val is_e_ts: term list -> bool + val itms2fstr: I_Model.single -> string * string + val par2fstr: I_Model.single -> string * TermC.as_string + val parsitm: theory -> I_Model.single -> I_Model.single + val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*) + (''a * string) list -> + (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*) +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) +end + +(**) +structure P_Spec(**): PRESENTATION_SPECIFICATION(**) = +struct +(**) + +fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e) + +(** handle an input P_Specific'action **) + +datatype iitem = + Given of TermC.as_string list +(*Where is still not input*) +| Find of TermC.as_string list +| Relate of TermC.as_string list + +type imodel = iitem list + +type icalhd = + Pos.pos' * (* the position in Ctree *) + TermC.as_string * (* the headline shown on Calc.T *) + imodel * (* the model *) + Pos.pos_ * (* model belongs to Problem or Method *) + References.T; (* into Know_Store *) +val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty) + +(* re-parse itms with a new thy and prepare for checking with ori list *) +fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) = + (let val t = Input_Descript.join (d, ts) + val _ = (UnparseC.term_in_thy dI t) + (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) + in itm end + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) + | parsitm dI (i, v, b, f, I_Model.Syn str) = + (let val _ = (Thm.term_of o the o (TermC.parse dI)) str + in (i, v, b ,f, I_Model.Par str) end + handle _ => (i, v, b, f, I_Model.Syn str)) + | parsitm dI (i, v, b, f, I_Model.Typ str) = + (let val _ = (Thm.term_of o the o (TermC.parse dI)) str + in (i, v, b, f, I_Model.Par str) end + handle _ => (i, v, b, f, I_Model.Syn str)) + | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) = + (let val t = Input_Descript.join (d,ts); + val _ = UnparseC.term_in_thy dI t; + (*this ^ should raise the exn on unability of re-parsing dts*) + in itm end + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) + | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) = + (let val t = Input_Descript.join (d,ts); + val _ = UnparseC.term_in_thy dI t; + (*this ^ should raise the exn on unability of re-parsing dts*) + in itm end + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) + | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) = + (let val t = d $ t'; + val _ = UnparseC.term_in_thy dI t; + (*this ^ should raise the exn on unability of re-parsing dts*) + in itm end + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) + | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) = + raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal"); + +(*separate a list to a pair of elements that do NOT satisfy the predicate, + and of elements that satisfy the predicate, i.e. (false, true)*) +fun filter_sep pred xs = + let + fun filt ab [] = ab + | filt (a, b) (x :: xs) = + if pred x + then filt (a, b @ [x]) xs + else filt (a @ [x], b) xs + in filt ([], []) xs end; +fun is_Par (_, _, _, _, I_Model.Par _) = true + | is_Par _ = false; + +fun is_e_ts [] = true + | is_e_ts [Const ("List.list.Nil", _)] = true + | is_e_ts _ = false; + +(* WN.9.11.03 copied from fun appl_add *) +fun appl_add' dI oris ppc pbt (sel, ct) = + let + val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt; + in + case TermC.parseNEW ctxt ct of + NONE => (0, [], false, sel, I_Model.Syn ct) + | SOME t => + (case I_Model.is_known ctxt sel oris t of + ("", ori', all) => + (case I_Model.is_notyet_input ctxt ppc all ori' pbt of + ("",itm) => itm + | (msg,_) => raise ERROR ("appl_add': " ^ msg)) + | (_, (i, v, _, d, ts), _) => + if is_e_ts ts + then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, []))) + else (i, v, false, sel, I_Model.Sup (d, ts))) + end + +(* generate preliminary itm_ from a strin (with field "#Given" etc.) *) +fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d'; +fun fstr2itm_ thy pbt (f, str) = + let + val topt = TermC.parse thy str + in + case topt of + NONE => ([], false, f, I_Model.Syn str) + | SOME ct => + let + val (d, ts) = (Input_Descript.split o Thm.term_of) ct + val popt = find_first (eq7 (f, d)) pbt + in + case popt of + NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts)) + | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts))) + end + end + +(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) +fun unknown_expl dI pbt selcts = + let + val thy = ThyC.get_theory dI + val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) + val its = O_Model.add_id its_ + in map flattup2 its end + +(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation + appl_add': generate 1 item + appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..) + appl_add' . is_notyet_input: compare with items in model already input + insert_ppc': insert this 1 item*) +fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts + (*already present itms in model are being overwritten*) + | appl_adds _ _ ppc _ [] = ppc + | appl_adds dI oris ppc pbt (selct :: ss) = + let val itm = appl_add' dI oris ppc pbt selct; + in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end + +fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s) + | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm) +fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts)) + | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str) + | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str) + | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts)) + | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts)) + | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t)) + | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) = + raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal"); + +fun imodel2fstr iitems = + let + fun xxx is [] = is + | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis + | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis + | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis + in xxx [] iitems end; + +(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *) +fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) = + let + val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of + Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), + spec = sspec as (sdI, spI, smI), probl, meth, ...} + => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) + | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p" + in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf)) + else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) + let val (pos_, pits, mits) = + if dI <> sdI + then let val its = map (parsitm (ThyC.get_theory dI)) probl; + val (its, trms) = filter_sep is_Par its; + val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec)) + in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end + else + if pI <> spI + then if pI = snd3 ospec then (Pos.Pbl, probl, meth) + else + let val pbt = (#ppc o Problem.from_store) pI + val dI' = #1 (References.select ospec spec) + val oris = if pI = #2 ospec then oris + else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*); + in (Pos.Pbl, appl_adds dI' oris probl pbt + (map itms2fstr probl), meth) end + else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) + then let val met = (#ppc o Method.from_store) mI + val mits = Specification.complete_metitms oris probl meth met + in if foldl and_ (true, map #3 mits) + then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) + end + else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)] + ((#ppc o Problem.from_store) (#2 (References.select ospec spec))) + (imodel2fstr imodel), meth) + val pt = Ctree.update_spec pt p spec; + in if pos_ = Pos.Pbl + then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec)) + val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits + in (Ctree.update_pbl pt p pits, + (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T) + end + else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec)) + val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits + in (Ctree.update_met pt p mits, + (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T) + end + end + end + | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl." + +(**)end (**) \ No newline at end of file diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/p-specific.sml --- a/src/Tools/isac/Specify/p-specific.sml Fri May 15 11:46:43 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,247 +0,0 @@ -(* Title: Specify/input-calchead.sml - Author: Walther Neuper - (c) due to copyright terms - -This will be dropped at switch to Isabelle/PIDE. -*) - -signature INPUT_SPECIFICATION = -sig - datatype iitem = - Find of TermC.as_string list - | Given of TermC.as_string list - | Relate of TermC.as_string list - type imodel = iitem list - type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) - (* NONE *) -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T -> - string * TermC.as_string -> I_Model.single - val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T -> - (string * TermC.as_string) list -> I_Model.T - val e_icalhd: icalhd - val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool - val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list - val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string -> - int list * bool * ''a * I_Model.feedback (*I_Model.single'*) - val imodel2fstr: iitem list -> (string * TermC.as_string) list - val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*) - val is_e_ts: term list -> bool - val itms2fstr: I_Model.single -> string * string - val par2fstr: I_Model.single -> string * TermC.as_string - val parsitm: theory -> I_Model.single -> I_Model.single - val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*) - (''a * string) list -> - (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*) -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) -end - -(**) -structure P_Specific(**): INPUT_SPECIFICATION(**) = -struct -(**) - -fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e) - -(** handle an input P_Specific'action **) - -datatype iitem = - Given of TermC.as_string list -(*Where is still not input*) -| Find of TermC.as_string list -| Relate of TermC.as_string list - -type imodel = iitem list - -type icalhd = - Pos.pos' * (* the position in Ctree *) - TermC.as_string * (* the headline shown on Calc.T *) - imodel * (* the model *) - Pos.pos_ * (* model belongs to Problem or Method *) - References.T; (* into Know_Store *) -val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty) - -(* re-parse itms with a new thy and prepare for checking with ori list *) -fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) = - (let val t = Input_Descript.join (d, ts) - val _ = (UnparseC.term_in_thy dI t) - (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) - in itm end - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) - | parsitm dI (i, v, b, f, I_Model.Syn str) = - (let val _ = (Thm.term_of o the o (TermC.parse dI)) str - in (i, v, b ,f, I_Model.Par str) end - handle _ => (i, v, b, f, I_Model.Syn str)) - | parsitm dI (i, v, b, f, I_Model.Typ str) = - (let val _ = (Thm.term_of o the o (TermC.parse dI)) str - in (i, v, b, f, I_Model.Par str) end - handle _ => (i, v, b, f, I_Model.Syn str)) - | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) = - (let val t = Input_Descript.join (d,ts); - val _ = UnparseC.term_in_thy dI t; - (*this ^ should raise the exn on unability of re-parsing dts*) - in itm end - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) - | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) = - (let val t = Input_Descript.join (d,ts); - val _ = UnparseC.term_in_thy dI t; - (*this ^ should raise the exn on unability of re-parsing dts*) - in itm end - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) - | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) = - (let val t = d $ t'; - val _ = UnparseC.term_in_thy dI t; - (*this ^ should raise the exn on unability of re-parsing dts*) - in itm end - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) - | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) = - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal"); - -(*separate a list to a pair of elements that do NOT satisfy the predicate, - and of elements that satisfy the predicate, i.e. (false, true)*) -fun filter_sep pred xs = - let - fun filt ab [] = ab - | filt (a, b) (x :: xs) = - if pred x - then filt (a, b @ [x]) xs - else filt (a @ [x], b) xs - in filt ([], []) xs end; -fun is_Par (_, _, _, _, I_Model.Par _) = true - | is_Par _ = false; - -fun is_e_ts [] = true - | is_e_ts [Const ("List.list.Nil", _)] = true - | is_e_ts _ = false; - -(* WN.9.11.03 copied from fun appl_add *) -fun appl_add' dI oris ppc pbt (sel, ct) = - let - val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt; - in - case TermC.parseNEW ctxt ct of - NONE => (0, [], false, sel, I_Model.Syn ct) - | SOME t => - (case I_Model.is_known ctxt sel oris t of - ("", ori', all) => - (case I_Model.is_notyet_input ctxt ppc all ori' pbt of - ("",itm) => itm - | (msg,_) => raise ERROR ("appl_add': " ^ msg)) - | (_, (i, v, _, d, ts), _) => - if is_e_ts ts - then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, []))) - else (i, v, false, sel, I_Model.Sup (d, ts))) - end - -(* generate preliminary itm_ from a strin (with field "#Given" etc.) *) -fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d'; -fun fstr2itm_ thy pbt (f, str) = - let - val topt = TermC.parse thy str - in - case topt of - NONE => ([], false, f, I_Model.Syn str) - | SOME ct => - let - val (d, ts) = (Input_Descript.split o Thm.term_of) ct - val popt = find_first (eq7 (f, d)) pbt - in - case popt of - NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts)) - | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts))) - end - end - -(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) -fun unknown_expl dI pbt selcts = - let - val thy = ThyC.get_theory dI - val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) - val its = O_Model.add_id its_ - in map flattup2 its end - -(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation - appl_add': generate 1 item - appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..) - appl_add' . is_notyet_input: compare with items in model already input - insert_ppc': insert this 1 item*) -fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts - (*already present itms in model are being overwritten*) - | appl_adds _ _ ppc _ [] = ppc - | appl_adds dI oris ppc pbt (selct :: ss) = - let val itm = appl_add' dI oris ppc pbt selct; - in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end - -fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s) - | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm) -fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts)) - | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str) - | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str) - | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts)) - | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts)) - | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t)) - | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) = - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal"); - -fun imodel2fstr iitems = - let - fun xxx is [] = is - | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis - | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis - | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis - in xxx [] iitems end; - -(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *) -fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) = - let - val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of - Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), - spec = sspec as (sdI, spI, smI), probl, meth, ...} - => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) - | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p" - in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf)) - else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) - let val (pos_, pits, mits) = - if dI <> sdI - then let val its = map (parsitm (ThyC.get_theory dI)) probl; - val (its, trms) = filter_sep is_Par its; - val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec)) - in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end - else - if pI <> spI - then if pI = snd3 ospec then (Pos.Pbl, probl, meth) - else - let val pbt = (#ppc o Problem.from_store) pI - val dI' = #1 (References.select ospec spec) - val oris = if pI = #2 ospec then oris - else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*); - in (Pos.Pbl, appl_adds dI' oris probl pbt - (map itms2fstr probl), meth) end - else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) - then let val met = (#ppc o Method.from_store) mI - val mits = Specification.complete_metitms oris probl meth met - in if foldl and_ (true, map #3 mits) - then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) - end - else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)] - ((#ppc o Problem.from_store) (#2 (References.select ospec spec))) - (imodel2fstr imodel), meth) - val pt = Ctree.update_spec pt p spec; - in if pos_ = Pos.Pbl - then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec)) - val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits - in (Ctree.update_pbl pt p pits, - (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T) - end - else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec)) - val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits - in (Ctree.update_met pt p mits, - (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T) - end - end - end - | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl." - -(**)end (**) \ No newline at end of file diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/refine.sml --- a/src/Tools/isac/Specify/refine.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/refine.sml Fri May 15 14:22:05 2020 +0200 @@ -13,7 +13,7 @@ val refine_ori' : O_Model.T -> Problem.id -> Problem.id (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) - val refine : Formalise.model -> Problem.id -> Model.match list + val refine : Formalise.model -> Problem.id -> M_Match.T list (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) (*NONE*) ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) @@ -132,11 +132,11 @@ (* refine a problem; construct pblRD while scanning *) fun refin pblRD ori (Store.Node (pI, [py], [])) = - if Model.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) + if M_Match.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) then SOME (pblRD @ [pI]) else NONE | refin pblRD ori (Store.Node (pI, [py], pys)) = - if Model.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) + if M_Match.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) then (case refins (pblRD @ [pI]) ori pys of SOME pblRD' => SOME pblRD' | NONE => SOME (pblRD @ [pI])) @@ -155,11 +155,11 @@ val {thy, ppc, where_, prls, ...} = py val oris = O_Model.init fmz thy ppc(* |> #1*); (* WN020803: itms!: oris might _not_ be complete here *) - val (b, (itms, pre')) = Model.match_oris' thy oris (ppc, where_, prls) + val (b, (itms, pre')) = M_Match.match_oris' thy oris (ppc, where_, prls) in if b - then pbls @ [Model.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')] - else pbls @ [Model.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')] + then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')] + else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')] end | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) = let @@ -167,13 +167,13 @@ val {thy, ppc, where_, prls, ...} = py val oris = O_Model.init fmz thy ppc(* |> #1*); (* WN020803: itms!: oris might _not_ be complete here *) - val(b, (itms, pre')) = Model.match_oris' thy oris (ppc,where_,prls); + val(b, (itms, pre')) = M_Match.match_oris' thy oris (ppc,where_,prls); in if b then - let val pbl = Model.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre') + let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre') in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end - else (pbls @ [Model.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]) + else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]) end | refin' _ _ _ _ = raise ERROR "refin': uncovered fun def." and refins' _ _ pbls [] = pbls @@ -182,8 +182,8 @@ val pbls' = refin' pblRD fmz pbls p in case last_elem pbls' of - Model.Matches _ => pbls' - | Model.NoMatch _ => refins' pblRD fmz pbls' pts + M_Match.Matches _ => pbls' + | M_Match.NoMatch _ => refins' pblRD fmz pbls' pts end; (* apply a fun to a ptyps node *) diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/specification.sml --- a/src/Tools/isac/Specify/specification.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/specification.sml Fri May 15 14:22:05 2020 +0200 @@ -54,51 +54,69 @@ (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName, add them to the model-pattern of met and let this input be done automatically; respective items must be in fmz. -#1# fmz contains items, which are stored in oris of the root(!)-problem. - This allows to specify methods, which require more input as anticipated - in writing partial_functions: such an item can be fetched from the root-problem's oris. - A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically - and thus is solved numerically. -#2# TODO *) signature SPECIFICATION = sig type T = Specification_Def.T - val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T -> - (string * (term * 'a)) list * (string * (term * 'b)) list -> References.T -> Pos.pos_ * Tactic.input - val reset_calchead : Calc.T -> Calc.T - val get_ocalhd : Calc.T -> T - val ocalhd_complete : I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool - val all_modspec : Calc.T -> Calc.T +(*val reset: Calc.T -> Calc.T*) + val reset_calchead: Calc.T -> Calc.T +(*val get: Calc.T -> T*) + val get_ocalhd: Calc.T -> T +(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*) + val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool +(*val is_complete: Calc.T -> bool*) + val is_complete_mod: Calc.T -> bool - val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T - val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T +(*/------- to Specify from Specification -------\*) +(*val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T -> + Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input*) + val nxt_spec: Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T -> + Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input +(*val do_all : Calc.T -> Calc.T*) + val all_modspec: Calc.T -> Calc.T +(*val finish_phase: Calc.T -> Calc.T*) + val complete_mod: Calc.T -> Calc.T +(*val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option*) + val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option +(*val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post*) + val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post +(*val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post*) + val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post +(*\------- to Specify from Specification -------/*) - val complete_mod : Calc.T -> Calc.T - val is_complete_mod : Calc.T -> bool - val complete_spec : Calc.T -> Calc.T - val is_complete_spec : Calc.T -> bool +(*/------- to References/\Def from Specification -------\*) +(*FIRST DO 1. References-> References_Def 2./Specify/references.sml*) +(*val complete: Calc.T -> Calc.T*) + val complete_spec: Calc.T -> Calc.T +(*val are_complete: Calc.T -> bool*) + val is_complete_spec: Calc.T -> bool +(*\------- to References/\Def from Specification -------/*) - val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T - val match_ags_msg : Problem.id -> term -> term list -> unit - val oris2fmz_vals : O_Model.T -> string list * term list - val vars_of_pbl_' : Model_Pattern.T -> term list +(*/------- to O_Model from Specification -------\*) + val match_ags: theory -> Model_Pattern.T -> term list -> O_Model.T + val match_ags_msg: Problem.id -> term -> term list -> unit + val oris2fmz_vals: O_Model.T -> string list * term list + val vars_of_pbl_': Model_Pattern.T -> term list +(*\------- to O_Model from Specification -------/*) - val ppc2list : 'a P_Model.ppc -> 'a list +(*/------- to I_Model from Specification -------\*) + val complete_metitms: O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T + val insert_ppc': I_Model.single -> I_Model.T -> I_Model.T + val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T -> + I_Model.T * I_Model.T + val is_error: I_Model.feedback -> bool + val itm_out: theory -> I_Model.feedback -> string + val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool +(*\------- to I_Model from Specification -------/*) - val itm_out : theory -> I_Model.feedback -> string +(*/------- to P_Model from Specification -------\*) + val ppc2list: 'a P_Model.ppc -> 'a list val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input val mk_additem: string -> TermC.as_string -> Tactic.input - val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option - val is_error: I_Model.feedback -> bool - val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T -> - I_Model.T * I_Model.T - val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post - val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post +(*\------- to P_Model from Specification -------/*) - val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) @@ -116,16 +134,16 @@ ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*) - val variants_in : term list -> int - val is_untouched : I_Model.single -> bool - val is_list_type : typ -> bool - val parse_ok : I_Model.feedback list -> bool - val all_dsc_in : I_Model.feedback list -> term list - val chktyps : theory -> term list * term list -> term list (* only in old tests*) - val is_complete_modspec : Calc.T -> bool - val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list -> + val variants_in: term list -> int + val is_untouched: I_Model.single -> bool + val is_list_type: typ -> bool + val parse_ok: I_Model.feedback list -> bool + val all_dsc_in: I_Model.feedback list -> term list + val chktyps: theory -> term list * term list -> term list (* only in old tests*) + val is_complete_modspec: Calc.T -> bool + val get_formress: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list -> (string * Pos.pos' * term) list - val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list -> + val get_forms: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list -> (string * Pos.pos' * term) list end @@ -273,7 +291,11 @@ | mk_additem "#Relate"ct = Tactic.Add_Relation ct | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"") -(* determine the next step of specification; +(*/------- to Specify from Specification -------\*) +(* + TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met + + determine the next step of specification; not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met)) eg. in rootpbl 'no_met': args: @@ -319,6 +341,7 @@ else if not preok then (Pos.Met, Tactic.Specify_Method mI) else (Pos.Met, Tactic.Apply_Method mI))) | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p) +(*\------- to Specify from Specification -------/*) (* make oris from args of the stac SubProblem and from pbt. can this formal argument (of a model-pattern) be omitted in the arg-list @@ -694,13 +717,16 @@ | is_complete_mod (_, pos) = raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)") -(* have (thy, pbl, met) _all_ been specified explicitly ? *) +(* have (thy, pbl, met) _all_ been specified explicitly ? RENAME References *) fun is_complete_spec (pt, pos as (p, _)) = - if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p - then raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos) + if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p then + raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos) else - let val (dI,pI,mI) = Ctree.get_obj Ctree.g_spec pt p - in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end + let + val (dI, pI, mI) = Ctree.get_obj Ctree.g_spec pt p + in (* vvv--- shift to References *) + dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty + end; (* complete empty items in specification from origin (pbl, met ev.refined); assumes 'is_complete_mod' *) diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/specify-step.sml --- a/src/Tools/isac/Specify/specify-step.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/specify-step.sml Fri May 15 14:22:05 2020 +0200 @@ -79,7 +79,7 @@ val {ppc, where_, prls, ...} = Problem.from_store pID; val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty then (false, (I_Model.init ppc, [])) - else Model.match_itms_oris thy itms (ppc, where_, prls) oris; + else M_Match.match_itms_oris thy itms (ppc, where_, prls) oris; in Applicable.Yes (Tactic.Specify_Problem' (pID, pbl)) end diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/specify.sml --- a/src/Tools/isac/Specify/specify.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/specify.sml Fri May 15 14:22:05 2020 +0200 @@ -1,4 +1,4 @@ -signature SPECIFY_NEW = +signature SPECIFY = sig val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input) (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) @@ -9,13 +9,14 @@ end (**) -structure Specify(**): SPECIFY_NEW(**) = +structure Specify(**): SPECIFY(**) = struct (**) open Pos open Ctree open Specification + fun find_next_step (pt, (p, p_)) = let val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/step-specify.sml --- a/src/Tools/isac/Specify/step-specify.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/step-specify.sml Fri May 15 14:22:05 2020 +0200 @@ -132,7 +132,7 @@ val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty then (false, (I_Model.init ppc, [])) - else Model.match_itms_oris thy probl (ppc,where_,prls) oris + else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*) val (c, pt) = case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of @@ -153,7 +153,7 @@ val thy = ThyC.get_theory dI val oris = O_Model.add thy ppc oris val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *) - val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris + val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc,pre,prls ) oris val itms = hack_until_review_Specify_2 mID itms val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos) @@ -249,7 +249,7 @@ val thy = ThyC.get_theory dI val oris = O_Model.add thy ppc oris val met = if met = [] then pbl else met - val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris + val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc, pre, prls) oris val itms = hack_until_review_Specify_1 mI' itms val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos) diff -r f1fdb213717b -r 08296690e7a6 src/Tools/isac/Specify/test-out.sml --- a/src/Tools/isac/Specify/test-out.sml Fri May 15 11:46:43 2020 +0200 +++ b/src/Tools/isac/Specify/test-out.sml Fri May 15 14:22:05 2020 +0200 @@ -54,7 +54,7 @@ Error_ of string (*<--*) | FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*) | PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.T) (*<--*) -| RefineKF of Model.match list (*<--*) +| RefineKF of M_Match.T list (*<--*) | RefinedKF of (Problem.id * ((I_Model.T) * (Pre_Conds.T))) (*<--*) datatype mout = diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri May 15 14:22:05 2020 +0200 @@ -266,7 +266,7 @@ text \\noindent Check if the given equation matches the specification of this equation type.\ ML \ - Model.match_pbl fmz (Problem.from_store ["univariate","equation"]); + M_Match.match_pbl fmz (Problem.from_store ["univariate","equation"]); \ text\\noindent We switch up to the {\sisac} Context and try to solve the @@ -290,7 +290,7 @@ specification of this equation type.\ ML \ - Model.match_pbl fmz (Problem.from_store + M_Match.match_pbl fmz (Problem.from_store ["abcFormula","degree_2","polynomial","univariate","equation"]); \ diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/BridgeLibisabelle/use-cases.sml --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 15 14:22:05 2020 +0200 @@ -894,8 +894,8 @@ modifyCalcHead 1 (([],Pbl),(*the position from refFormula*) "solve (x+1=2, x)",(*the headline*) - [P_Specific.Given ["equality (x+1=(2::real))", "solveFor x"], - P_Specific.Find ["solutions L"](*,P_Specific.Relate []*)], + [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"], + P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)], Pbl, ("Test", ["sqroot-test","univariate","equation","test"], @@ -961,9 +961,9 @@ val spec = ("DiffApp", ["maximum_of","function"], ["DiffApp","max_by_calculus"]); (*the empty model with descriptions for user-guidance by Model_Problem*) - val empty_model = [P_Specific.Given ["fixedValues []"], - P_Specific.Find ["maximum", "valuesFor"], - P_Specific.Relate ["relations []"]]; + val empty_model = [P_Spec.Given ["fixedValues []"], + P_Spec.Find ["maximum", "valuesFor"], + P_Spec.Relate ["relations []"]]; DEconstrCalcTree 1; "#################################################################"; @@ -985,9 +985,9 @@ modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*), "Problem (DiffApp.thy, [maximum_of, function])", (*the head-form ^^^ is not used for input here*) - [P_Specific.Given ["fixedValues [r=Arbfix]"(*new input*)], - P_Specific.Find ["maximum b"(*new input*), "valuesFor"], - P_Specific.Relate ["relations"]], + [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)], + P_Spec.Find ["maximum b"(*new input*), "valuesFor"], + P_Spec.Relate ["relations"]], (*input (Arbfix will dissappear soon)*) Pbl (*belongsto*), References.empty (*no input to the specification*)); @@ -1001,30 +1001,30 @@ (*this input completes the model*) modifyCalcHead 1 (([],Pbl), "not used here", - [P_Specific.Given ["fixedValues [r=Arbfix]"], - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)], - P_Specific.Relate ["relations [A=a*b, \ + [P_Spec.Given ["fixedValues [r=Arbfix]"], + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], + P_Spec.Relate ["relations [A=a*b, \ \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, References.empty); (*specification is not interesting and should be skipped by the dialogguide; !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*) modifyCalcHead 1 (([],Pbl), "not used here", - [P_Specific.Given ["fixedValues [r=Arbfix]"], - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)], - P_Specific.Relate ["relations [A=a*b, \ + [P_Spec.Given ["fixedValues [r=Arbfix]"], + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], + P_Spec.Relate ["relations [A=a*b, \ \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, ("DiffApp", ["empty_probl_id"], ["empty_meth_id"])); modifyCalcHead 1 (([],Pbl), "not used here", - [P_Specific.Given ["fixedValues [r=Arbfix]"], - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)], - P_Specific.Relate ["relations [A=a*b, \ + [P_Spec.Given ["fixedValues [r=Arbfix]"], + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], + P_Spec.Relate ["relations [A=a*b, \ \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, ("DiffApp", ["maximum_of","function"], ["empty_meth_id"])); modifyCalcHead 1 (([],Pbl), "not used here", - [P_Specific.Given ["fixedValues [r=Arbfix]"], - P_Specific.Find ["maximum A", "valuesFor [a,b]"(*new input*)], - P_Specific.Relate ["relations [A=a*b, \ + [P_Spec.Given ["fixedValues [r=Arbfix]"], + P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], + P_Spec.Relate ["relations [A=a*b, \ \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, ("DiffApp", ["maximum_of","function"], ["DiffApp","max_by_calculus"])); @@ -1040,8 +1040,8 @@ Iterator 1; moveActiveRoot 1; refFormula 1 (get_pos 1 1); modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))", - [P_Specific.Given ["equality (1+-1*2+x=(0::real))", "solveFor x"], - P_Specific.Find ["solutions L"]], + [P_Spec.Given ["equality (1+-1*2+x=(0::real))", "solveFor x"], + P_Spec.Find ["solutions L"]], Pbl, ("Test", ["LINEAR","univariate","equation","test"], ["Test","solve_linear"])); diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Knowledge/eqsystem.sml --- a/test/Tools/isac/Knowledge/eqsystem.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri May 15 14:22:05 2020 +0200 @@ -316,10 +316,10 @@ "===== case 1 ====="; val matches = Refine.refine fmz ["LINEAR","system"]; case matches of - [Model.Matches (["LINEAR", "system"], _), - Model.Matches (["2x2", "LINEAR", "system"], _), - Model.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), - Model.Matches (["normalise", "2x2", "LINEAR", "system"], + [M_Match.Matches (["LINEAR", "system"], _), + M_Match.Matches (["2x2", "LINEAR", "system"], _), + M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), + M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], {Find = [Correct "solution LL"], With = [], Given = @@ -335,7 +335,7 @@ "solveForVars [c, c_2]", "solution LL"]; val matches = Refine.refine fmz ["LINEAR","system"]; case matches of [_,_, - Model.Matches + M_Match.Matches (["triangular", "2x2", "LINEAR", "system"], {Find = [Correct "solution LL"], With = [], @@ -391,13 +391,13 @@ \-------------------------------------------------------/ val matches = Refine.refine fmz ["LINEAR","system"]; case matches of - [Model.Matches (["LINEAR", "system"], _), - Model.NoMatch (["2x2", "LINEAR", "system"], _), - Model.NoMatch (["3x3", "LINEAR", "system"], _), - Model.Matches (["4x4", "LINEAR", "system"], _), - Model.NoMatch (["triangular", "4x4", "LINEAR", "system"], _), - Model.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => () - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys Model.NoMatch"; + [M_Match.Matches (["LINEAR", "system"], _), + M_Match.NoMatch (["2x2", "LINEAR", "system"], _), + M_Match.NoMatch (["3x3", "LINEAR", "system"], _), + M_Match.Matches (["4x4", "LINEAR", "system"], _), + M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _), + M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => () + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch"; (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*) "===== case 4 ====="; @@ -408,8 +408,8 @@ "solveForVars [c, c_2, c_3, c_4]", "solution LL"]; val matches = Refine.refine fmz ["triangular", "4x4", "LINEAR","system"]; case matches of - [Model.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => () - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys Model.NoMatch"; + [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => () + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch"; val matches = Refine.refine fmz ["LINEAR","system"]; ============ inhibit exn WN120314 ==============================================*) diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Knowledge/poly.sml Fri May 15 14:22:05 2020 +0200 @@ -565,7 +565,7 @@ val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"]; "-----0 ---"; case Refine.refine fmz ["polynomial","simplification"]of - [Model.Matches (["polynomial", "simplification"], _)] => () + [M_Match.Matches (["polynomial", "simplification"], _)] => () | _ => error "poly.sml diff.behav. in check pbl, Refine.refine"; (*...if there is an error, then ...*) @@ -574,12 +574,12 @@ val pbt = Problem.from_store ["polynomial","simplification"]; (*default_print_depth 3;*) (*if there is ... -> val Model.NoMatch' {Given=gi, Where=wh, Find=fi,...} = Model.match_pbl fmz pbt; +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt; ... then Rewrite.trace_on:*) "-----2 ---"; Rewrite.trace_on := false; -Model.match_pbl fmz pbt; +M_Match.match_pbl fmz pbt; Rewrite.trace_on := false; (*... if there is no rewrite, then there is something wrong with prls*) @@ -596,10 +596,10 @@ "-----4 ---"; (*show_types:=true;*) (* -> val Model.NoMatch' {Given=gi, Where=wh, Find=fi,...} = Model.match_pbl fmz pbt; +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt; val wh = [False "(t_::real => real) (is_polyexp::real)"] ......................^^^^^^^^^^^^...............^^^^*) -val Model.Matches' _ = Model.match_pbl fmz pbt; +val M_Match.Matches' _ = M_Match.match_pbl fmz pbt; (*show_types:=false;*) diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Knowledge/polyeq-1.sml --- a/test/Tools/isac/Knowledge/polyeq-1.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Fri May 15 14:22:05 2020 +0200 @@ -109,22 +109,22 @@ "----------- test matching problems --------------------------0---"; "----------- test matching problems --------------------------0---"; val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"]; -if Model.match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) = - Model.Matches' {Find = [Correct "solutions L"], +if M_Match.match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) = + M_Match.Matches' {Find = [Correct "solutions L"], With = [], Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)", Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"], Relate = []} -then () else error "Model.match_pbl [expanded,univariate,equation]"; +then () else error "M_Match.match_pbl [expanded,univariate,equation]"; -if Model.match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) = - Model.Matches' {Find = [Correct "solutions L"], +if M_Match.match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) = + M_Match.Matches' {Find = [Correct "solutions L"], With = [], Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"], Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*) -then () else error "Model.match_pbl [degree_2,expanded,univariate,equation]"; +then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]"; "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri May 15 14:22:05 2020 +0200 @@ -40,13 +40,13 @@ val result = UnparseC.term t_; if result <> "True" then error "rateq.sml: new behaviour 4:" else (); -val result = Model.match_pbl ["equality (x=(1::real))","solveFor x","solutions L"] +val result = M_Match.match_pbl ["equality (x=(1::real))","solveFor x","solutions L"] (Problem.from_store ["rational","univariate","equation"]); -case result of Model.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5"; +case result of M_Match.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5"; -val result = Model.match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] +val result = M_Match.match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] (Problem.from_store ["rational","univariate","equation"]); -case result of Model.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6"; +case result of M_Match.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6"; "------------ solve (1/x = 5, x) by me ---------------------------"; "------------ solve (1/x = 5, x) by me ---------------------------"; diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Knowledge/rooteq.sml --- a/test/Tools/isac/Knowledge/rooteq.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Knowledge/rooteq.sml Fri May 15 14:22:05 2020 +0200 @@ -84,13 +84,13 @@ -val result = Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] +val result = M_Match.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation"]); -case result of Model.Matches' _ => () | _ => error "rooteq.sml: new behaviour:"; +case result of M_Match.Matches' _ => () | _ => error "rooteq.sml: new behaviour:"; -val result = Model.match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"] +val result = M_Match.match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation"]); -case result of Model.NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:"; +case result of M_Match.NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:"; (*---------rooteq---- 23.8.02 ---------------------*) "---------(1/sqrt(x)=5)---------------------"; @@ -778,6 +778,6 @@ Refine.refine fmz ["univariate","equation","test"]; -Model.match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]); +M_Match.match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]); ===== copied here from OLDTESTS in case there is a Program ===^^^=============================*) diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/OLDTESTS/script_if.sml --- a/test/Tools/isac/OLDTESTS/script_if.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Fri May 15 14:22:05 2020 +0200 @@ -65,7 +65,7 @@ [("Test","methode")])] thy; -Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]); +M_Match.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]); KEStore_Elems.add_pbts [Problem.prep_input (theory "Isac_Knowledge") diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Specify/m-match.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Specify/m-match.sml Fri May 15 14:22:05 2020 +0200 @@ -0,0 +1,17 @@ +(* Title: "Specify/model.sml" + Author: Walther Neuper + (c) due to copyright terms +*) + +"-----------------------------------------------------------------------------------------------"; +"table of contents -----------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"----------- TODO ------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; + +open M_Match; +"----------- TODO ------------------------------------------------------------------------------"; +"----------- TODO ------------------------------------------------------------------------------"; +"----------- TODO ------------------------------------------------------------------------------"; diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Specify/model.sml --- a/test/Tools/isac/Specify/model.sml Fri May 15 11:46:43 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: "Specify/model.sml" - Author: Walther Neuper - (c) due to copyright terms -*) - -"-----------------------------------------------------------------------------------------------"; -"table of contents -----------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"----------- TODO ------------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; - -open Model; -"----------- TODO ------------------------------------------------------------------------------"; -"----------- TODO ------------------------------------------------------------------------------"; -"----------- TODO ------------------------------------------------------------------------------"; diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Specify/ptyps.sml --- a/test/Tools/isac/Specify/ptyps.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Specify/ptyps.sml Fri May 15 14:22:05 2020 +0200 @@ -138,7 +138,7 @@ "solveFor x","errorBound (eps=0)","solutions L"]; val pbt as {thy = thy, where_ = pre, ppc = ppc,...} = Problem.from_store ["univariate","equation"]; -Model.match_pbl fmz pbt; +M_Match.match_pbl fmz pbt; *) "----------- fun match_oris --------------------------------------"; "----------- fun match_oris --------------------------------------"; diff -r f1fdb213717b -r 08296690e7a6 test/Tools/isac/Specify/refine.sml --- a/test/Tools/isac/Specify/refine.sml Fri May 15 11:46:43 2020 +0200 +++ b/test/Tools/isac/Specify/refine.sml Fri May 15 14:22:05 2020 +0200 @@ -116,10 +116,10 @@ (*case 1: no refinement *) case Refine.refine fmz1 ["pbla", "refine", "test"] of - [Model.Matches (["pbla", "refine", "test"], _), - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => () + [M_Match.Matches (["pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => () | _ => error "--- Refine.refine test-pbtyps --- broken with case 1"; (* *** pass ["pbla"] @@ -127,22 +127,22 @@ *** pass ["pbla","pbla2"] *** pass ["pbla","pbla3"] val it = - [Model.Matches + [M_Match.Matches (["pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]", Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla1","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_", Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla3","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_", @@ -151,10 +151,10 @@ (*case 2: refined to pbt without children *) case Refine.refine fmz2 ["pbla", "refine", "test"] of - [Model.Matches (["pbla", "refine", "test"], _), - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2", "pbla", "refine", "test"], _), - Model.Matches (["pbla3", "pbla", "refine", "test"], _)] => () + [M_Match.Matches (["pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _), + M_Match.Matches (["pbla3", "pbla", "refine", "test"], _)] => () | _ => error "--- Refine.refine test-pbtyps --- broken with case 2"; (* *** pass ["pbla"] @@ -162,22 +162,22 @@ *** pass ["pbla","pbla2"] *** pass ["pbla","pbla3"] val it = - [Model.Matches + [M_Match.Matches (["pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"], Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla1","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", Superfl "relations aaa333"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_", Superfl "relations aaa333"],Relate=[],Where=[],With=[]}), - Model.Matches + M_Match.Matches (["pbla3","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"], @@ -185,13 +185,13 @@ (*case 3: refined to pbt with children *) case Refine.refine fmz3 ["pbla", "refine", "test"] of - [Model.Matches (["pbla", "refine", "test"], _), - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _), - Model.Matches (["pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => () + [M_Match.Matches (["pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _), + M_Match.Matches (["pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => () | _ => error "--- Refine.refine test-pbtyps --- broken with case 3"; (* *** pass ["pbla"] @@ -202,37 +202,37 @@ *** pass ["pbla","pbla2","pbla2z"] *** pass ["pbla","pbla3"] val it = - [Model.Matches + [M_Match.Matches (["pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"], Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla1","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}), - Model.Matches + M_Match.Matches (["pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"], Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2x","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2y","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2z","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Missing "interval a2z_"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla3","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_", @@ -241,11 +241,11 @@ (*case 4: refined to children (without child)*) case Refine.refine fmz4 ["pbla", "refine", "test"] of - [Model.Matches (["pbla", "refine", "test"], _), - Model.NoMatch (["pbla1", "pbla", "refine", "test"], _), - Model.Matches (["pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), - Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => () + [M_Match.Matches (["pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _), + M_Match.Matches (["pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), + M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => () | _ => error "--- Refine.refine test-pbtyps --- broken with case 4"; (* *** pass ["pbla"] @@ -254,29 +254,29 @@ *** pass ["pbla","pbla2","pbla2x"] *** pass ["pbla","pbla2","pbla2y"] val it = - [Model.Matches + [M_Match.Matches (["pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222", Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla1","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"], Relate=[],Where=[],With=[]}), - Model.Matches + M_Match.Matches (["pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2x","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"], Relate=[],Where=[],With=[]}), - Model.Matches + M_Match.Matches (["pbla2y","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", @@ -285,27 +285,27 @@ (*case 5: start refinement somewhere in ptyps*) case Refine.refine fmz4 ["pbla2","pbla", "refine", "test"] of - [Model.Matches (["pbla2", "pbla", "refine", "test"], _), - Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), - Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => () + [M_Match.Matches (["pbla2", "pbla", "refine", "test"], _), + M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), + M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => () | _ => error "--- Refine.refine test-pbtyps --- broken with case 5"; (* *** pass ["pbla","pbla2"] *** pass ["pbla","pbla2","pbla2x"] *** pass ["pbla","pbla2","pbla2y"] val it = - [Model.Matches + [M_Match.Matches (["pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), - Model.NoMatch + M_Match.NoMatch (["pbla2x","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"], Relate=[],Where=[],With=[]}), - Model.Matches + M_Match.Matches (["pbla2y","pbla2","pbla"], {Find=[], Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",