929 |
929 |
930 (*.can this formal argument (of a model-pattern) be omitted in the arg-list |
930 (*.can this formal argument (of a model-pattern) be omitted in the arg-list |
931 of a SubProblem ? see ME/ptyps.sml 'type met '.*) |
931 of a SubProblem ? see ME/ptyps.sml 'type met '.*) |
932 fun is_copy_named_idstr str = |
932 fun is_copy_named_idstr str = |
933 case (rev o explode) str of |
933 case (rev o explode) str of |
934 (*"_"::_ ::"_"::_ => true*) |
934 (*"_":: _ ::"_"::_ => true*) |
935 "'"::"'"::"'"::_ => true |
935 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) str ^ " T"); |
936 | _ => false; |
936 true) |
937 (*> is_copy_named_idstr "v_i'''"; |
937 | _ => (tracing ((strs2str o (rev o explode)) str ^ " F"); false); |
938 val it = true : bool |
938 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t; |
939 > is_copy_named_idstr "e_"; |
939 |
940 val it = false : bool |
|
941 > is_copy_named_idstr "L___"; |
|
942 val it = true : bool |
|
943 *) |
|
944 (*.should this formal argument (of a model-pattern) create a new identifier?.*) |
940 (*.should this formal argument (of a model-pattern) create a new identifier?.*) |
945 fun is_copy_named_generating_idstr str = |
941 fun is_copy_named_generating_idstr str = |
946 if is_copy_named_idstr str |
942 if is_copy_named_idstr str |
947 then case (rev o explode) str of |
943 then case (rev o explode) str of |
948 "_"::"_"::"_"::_ => false |
944 (*"_"::"_"::"_"::_ => false*) |
|
945 "'"::"'"::"'"::_ => false |
949 | _ => true |
946 | _ => true |
950 else false; |
947 else false; |
951 (*> is_copy_named_generating_idstr "v_i'''"; |
948 fun is_copy_named_generating (_, (_, t)) = |
952 val it = true : bool |
|
953 > is_copy_named_generating_idstr "L___"; |
|
954 val it = false : bool |
|
955 *) |
|
956 |
|
957 (*.can this formal argument (of a model-pattern) be omitted in the arg-list |
|
958 of a SubProblem ? see ME/ptyps.sml 'type met '.*) |
|
959 fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t; |
|
960 (*.should this formal argument (of a model-pattern) create a new identifier?.*) |
|
961 fun is_copy_named_generating (_,(_,t)) = |
|
962 (is_copy_named_generating_idstr o free2str) t; |
949 (is_copy_named_generating_idstr o free2str) t; |
963 |
|
964 |
950 |
965 (*.split type-wrapper from scr-arg and build part of an ori; |
951 (*.split type-wrapper from scr-arg and build part of an ori; |
966 an type-error is reported immediately, raises an exn, |
952 an type-error is reported immediately, raises an exn, |
967 subsequent handling of exn provides 2nd part of error message.*) |
953 subsequent handling of exn provides 2nd part of error message.*) |
968 (*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term |
954 (*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term |