1 (* Title: BaseDefinitions/model-pattern.sml
3 (c) due to copyright terms
5 A \<open>Model_Pattern\<close> defines a -> \<open>Problem\<close>-type: its \<open>variables\<close> are to be instantiated
6 by the values for particular \<open>Problem\<close>s.
7 The \<open>variables\<close> are used twice, in a model and as formal arguments in a \<open>Program\<close>.
8 The \<open>descriptor\<close>s are unique identifiers within one \<open>Model_Pattern\<close>.
10 signature MODEL_PATTERN =
14 val to_string: single list -> string
16 type descriptor = term
18 val variables: T -> term list
19 val get_field: descriptor -> T -> m_field option
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
21 val to_string': T -> string
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28 structure Model_Pattern(**): MODEL_PATTERN(**) =
32 (* the pattern for an item of a problems model or a methods guard *)
33 type m_field = string;
34 type descriptor = term;
36 (m_field * (* field Given, Find, Relate *)
37 (descriptor * (* for snd term *)
38 term)) (* id | arbitrary term *);
41 fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
42 fun to_string pats = (strs2str o (map pat2str)) pats;
43 fun pat2str' (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n";
44 fun to_string' pats = (strs2str o (map pat2str')) pats;
46 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
49 fun var_of_pbl_ (_, (_, t)) = t: term
50 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
52 fun get_field descriptor m_patt =
53 (filter ((curry (fn (desc, (_, (desc', _))) => desc = desc')) descriptor) m_patt
55 |> (fn (a, _) => SOME a))
56 handle List.Empty => NONE