962 val mvat = max_vt itms; |
962 val mvat = max_vt itms; |
963 val complete = chk1_mis mvat itms pbt; |
963 val complete = chk1_mis mvat itms pbt; |
964 val pre' = check_preconds' prls pre itms mvat |
964 val pre' = check_preconds' prls pre itms mvat |
965 val pb = foldl and_ (true, map fst pre') |
965 val pb = foldl and_ (true, map fst pre') |
966 in if complete andalso pb then true else false end; |
966 in if complete andalso pb then true else false end; |
967 (*run subp-rooteq.sml 'root-eq + subpbl: solve_linear' |
|
968 until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"... |
|
969 > val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_, |
|
970 Nd(PblObj{origin=(oris,_,_),...},[])]) = pt; |
|
971 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"], |
|
972 (#where_ o get_pbt) ["linear","univariate","equation"]); |
|
973 > match_oris oris (pbt,pre); |
|
974 val it = true : bool |
|
975 |
|
976 |
|
977 > val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"], |
|
978 (#where_ o get_pbt)["plain_square","univariate","equation"]); |
|
979 > match_oris oris (pbt,pre); |
|
980 val it = false : bool |
|
981 |
|
982 |
|
983 --------------------------------------------------- |
|
984 run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square' |
|
985 until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ... |
|
986 > val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]), |
|
987 Nd (PblObj {origin=(oris,_,_),...},[])]) = pt; |
|
988 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"], |
|
989 (#where_ o get_pbt) ["linear","univariate","equation"]); |
|
990 > match_oris oris (pbt,pre); |
|
991 val it = false : bool |
|
992 |
|
993 |
|
994 > val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"], |
|
995 (#where_ o get_pbt) ["plain_square","univariate","equation"]); |
|
996 > match_oris oris (pbt,pre); |
|
997 val it = true : bool |
|
998 *) |
|
999 (*^^^--- doubled 20.9.01 *) |
|
1000 |
|
1001 |
967 |
1002 (*. check a problem (ie. ori list) for matching a problemtype, |
968 (*. check a problem (ie. ori list) for matching a problemtype, |
1003 returns items for output to math-experts .*) |
969 returns items for output to math-experts .*) |
1004 (* val (ppc,pre) = (#ppc py, #where_ py); |
|
1005 *) |
|
1006 fun match_oris' thy oris (ppc,pre,prls) = |
970 fun match_oris' thy oris (ppc,pre,prls) = |
1007 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls)); |
971 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls)); |
1008 *) |
972 *) |
1009 let val itms = (flat o (map (chk1_ thy ppc))) oris; |
973 let val itms = (flat o (map (chk1_ thy ppc))) oris; |
1010 val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris; |
974 val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris; |
1012 val miss = chk1_mis' oris ppc; |
976 val miss = chk1_mis' oris ppc; |
1013 val pre' = check_preconds' prls pre itms mvat |
977 val pre' = check_preconds' prls pre itms mvat |
1014 val pb = foldl and_ (true, map fst pre') |
978 val pb = foldl and_ (true, map fst pre') |
1015 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; |
979 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; |
1016 |
980 |
1017 (*. for the user .*) |
981 (* for the user *) |
1018 datatype match' = |
982 datatype match' = |
1019 Matches' of item ppc |
983 Matches' of item ppc |
1020 | NoMatch' of item ppc; |
984 | NoMatch' of item ppc; |
1021 |
985 |
1022 (*. match a formalization with a problem type .*) |
986 (* match a formalization with a problem type *) |
1023 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) = |
987 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) = |
1024 let val oris = prep_ori fmz thy ppc |> #1; |
988 let val oris = prep_ori fmz thy ppc |> #1; |
1025 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er); |
989 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er); |
1026 in if bool then Matches' (itms2itemppc thy itms pre') |
990 in if bool then Matches' (itms2itemppc thy itms pre') |
1027 else NoMatch' (itms2itemppc thy itms pre') end; |
991 else NoMatch' (itms2itemppc thy itms pre') end; |