test/Tools/isac/Knowledge/polyeq-1.sml
changeset 60556 486223010ea8
parent 60509 2e0b7ca391dc
child 60559 aba19e46dd84
equal deleted inserted replaced
60555:466bcb20f2d7 60556:486223010ea8
   107 
   107 
   108 "----------- test matching problems --------------------------0---";
   108 "----------- test matching problems --------------------------0---";
   109 "----------- test matching problems --------------------------0---";
   109 "----------- test matching problems --------------------------0---";
   110 "----------- test matching problems --------------------------0---";
   110 "----------- test matching problems --------------------------0---";
   111 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
   111 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
   112 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
   112 if M_Match.match_pbl fmz (Problem.from_store_PIDE @{context} ["expanded", "univariate", "equation"]) =
   113   M_Match.Matches' {Find = [Correct "solutions L"], 
   113   M_Match.Matches' {Find = [Correct "solutions L"], 
   114             With = [], 
   114             With = [], 
   115             Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
   115             Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
   116             Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)", 
   116             Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)", 
   117                      Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], 
   117                      Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], 
   118             Relate = []}
   118             Relate = []}
   119 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
   119 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
   120 
   120 
   121 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
   121 if M_Match.match_pbl fmz (Problem.from_store_PIDE @{context} ["degree_2", "expanded", "univariate", "equation"]) =
   122   M_Match.Matches' {Find = [Correct "solutions L"], 
   122   M_Match.Matches' {Find = [Correct "solutions L"], 
   123             With = [], 
   123             With = [], 
   124             Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
   124             Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
   125             Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], 
   125             Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], 
   126             Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)
   126             Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)