47 val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list |
47 val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list |
48 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T |
48 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T |
49 -> message * single |
49 -> message * single |
50 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string |
50 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string |
51 |
51 |
52 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST -> |
52 (* |
53 Model_Def.i_model_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval) |
53 val of_max_variant: Model_Pattern.T -> T_TEST -> |
54 |
54 T_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval) |
|
55 *) |
|
56 val of_max_variant: Model_Pattern.T -> T_TEST -> |
|
57 (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval) |
|
58 |
|
59 (*REN make_complete*) |
55 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T |
60 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T |
56 val add: single -> T -> T |
61 val add: single -> T -> T |
57 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T |
62 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T |
58 val is_error: feedback -> bool |
63 val is_error: feedback -> bool |
|
64 (*REN complete_internal*) |
59 val complete': Model_Pattern.T -> O_Model.single -> single |
65 val complete': Model_Pattern.T -> O_Model.single -> single |
60 |
66 |
61 val is_complete: T -> bool |
67 val is_complete: T -> bool |
62 val is_complete_variant: int -> T_TEST-> bool |
68 val is_complete_variant: Model_Def.variant -> T_TEST-> bool |
63 val to_p_model: theory -> feedback -> string |
69 val to_p_model: theory -> feedback -> string |
|
70 |
|
71 (*from isac_test for Minisubpbl*) |
64 val eq1: ''a -> 'b * (''a * 'c) -> bool |
72 val eq1: ''a -> 'b * (''a * 'c) -> bool |
65 |
73 val filter_outs: O_Model.T -> T -> O_Model.T |
66 (*from isac_test for Minisubpbl*) |
74 val filter_outs_TEST: O_Model.T -> T_TEST -> O_Model.T |
67 val feedback_to_string: Proof.context -> feedback -> string |
75 val feedback_to_string: Proof.context -> feedback -> string |
68 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string |
76 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string |
69 |
77 |
70 val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list -> |
78 val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list -> |
71 'a * 'b * bool * string * feedback |
79 'a * 'b * bool * string * feedback |
397 ))\<close> of |
405 ))\<close> of |
398 SOME x => x |
406 SOME x => x |
399 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts))) |
407 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts))) |
400 |
408 |
401 (*filter out oris which have same description in itms*) |
409 (*filter out oris which have same description in itms*) |
|
410 (* ---------------------------------- type problems ---vv---------vv |
402 fun filter_outs oris [] = oris |
411 fun filter_outs oris [] = oris |
403 | filter_outs oris (i::itms) = |
412 | filter_outs oris (i::itms) = |
404 let |
413 let |
405 val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris |
414 val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris |
406 in |
415 in |
407 filter_outs ors itms |
416 filter_outs ors itms |
408 end |
417 end |
|
418 *) |
|
419 (*with types..*) |
|
420 (*T_TESTold*) |
|
421 fun filter_outs oris [] = oris |
|
422 | filter_outs oris (i::itms) = |
|
423 let |
|
424 val ors = filter_out ((curry op = ((descriptor o |
|
425 (#5: single -> feedback)) i)) o |
|
426 (#4: O_Model.single -> O_Model.descriptor)) oris |
|
427 in |
|
428 filter_outs ors itms |
|
429 end |
|
430 (*T_TEST*) |
|
431 fun filter_outs_TEST oris [] = oris |
|
432 | filter_outs_TEST oris (i::itms) = |
|
433 let |
|
434 val ors = filter_out ((curry op = ((descriptor_TEST o |
|
435 ((#1 o #5): single_TEST -> feedback_TEST) ) i) ) o |
|
436 (#4: O_Model.single -> O_Model.descriptor) ) oris |
|
437 in |
|
438 filter_outs_TEST ors itms |
|
439 end |
|
440 (*T_TESTnew*) |
409 |
441 |
410 (*filter oris which are in pbt, too*) |
442 (*filter oris which are in pbt, too*) |
411 fun filter_pbt oris pbt = |
443 fun filter_pbt oris pbt = |
412 let |
444 let |
413 val dscs = map (fst o snd) pbt |
445 val dscs = map (fst o snd) pbt |
446 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*) |
478 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*) |
447 in |
479 in |
448 itms @ (map (complete' met) os) |
480 itms @ (map (complete' met) os) |
449 end |
481 end |
450 |
482 |
451 (*complete model and guard of a calc-head*) |
483 (*complete model and guard of a calc-head WN230829 replaced by complete_pos*) |
452 fun complete_method (oris, mpc, model, probl) = |
484 fun complete_method (oris, mpc, model, probl) = |
453 let |
485 let |
454 val pits = filter_out ((curry op= false) o (#3)) probl |
486 val pits = filter_out ((curry op= false) o (#3)) probl |
455 val vat = if probl = [] then 1 else Pre_Conds.max_variant probl |
487 val vat = if probl = [] then 1 else Pre_Conds.max_variant probl |
456 val pors = filter ((member_swap op = vat) o (#2)) oris |
488 val pors = filter ((member_swap op = vat) o (#2)) oris |
462 |
494 |
463 (*TODO: also check if all elements are I_Model.Cor*) |
495 (*TODO: also check if all elements are I_Model.Cor*) |
464 fun is_complete ([]: T) = false |
496 fun is_complete ([]: T) = false |
465 | is_complete itms = foldl and_ (true, (map #3 itms)) |
497 | is_complete itms = foldl and_ (true, (map #3 itms)) |
466 |
498 |
467 (*for PIDE*) |
499 (*for PIDE: are all feedback Cor ? MISSING: Pre_Conds.check *) |
468 fun is_complete_variant no_model_items i_model = |
500 fun is_complete_variant no_model_items i_model = |
469 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model) |
501 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model) |
470 |
502 |
471 val of_max_variant = Pre_Conds.of_max_variant |
503 val of_max_variant = Pre_Conds.of_max_variant |
472 |
504 |