src/Tools/isac/BaseDefinitions/model-pattern.sml
changeset 59945 bdc420a363d8
parent 59914 ab5bd5c37e13
child 59947 3df8a1d00a24
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml	Thu May 07 11:42:19 2020 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +(* Title:  BaseDefinitions/model-pattern.sml
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +A pattern to be combined with a formalisation (Formalise.T) yielding an O_Model.T..
     1.9 +*)
    1.10 +signature MODEL_PATTERN =
    1.11 +sig
    1.12 +  type T
    1.13 +(*type pat*)
    1.14 +  type single
    1.15 +(*val pats2str: single list -> string*)
    1.16 +  val to_string: single list -> string
    1.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.18 +(*val pats2str': single list -> string*)
    1.19 +  val to_string': single list -> string
    1.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.21 +  (*NONE*)                                                                      
    1.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.23 +end
    1.24 +
    1.25 +(**)
    1.26 +structure Model_Pattern(**): MODEL_PATTERN(**) =
    1.27 +struct
    1.28 +(**)
    1.29 +
    1.30 +(* the pattern for an item of a problems model or a methods guard *)
    1.31 +type m_field = string;
    1.32 +type single =
    1.33 +  (m_field *     (* field               *)
    1.34 +	  (term *     (* description         *)
    1.35 +	     term))   (* id | arbitrary term *);
    1.36 +type T = single list;
    1.37 +
    1.38 +fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
    1.39 +fun to_string pats = (strs2str o (map pat2str)) pats;
    1.40 +fun pat2str' (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n";
    1.41 +fun to_string' pats = (strs2str o (map pat2str')) pats;
    1.42 +
    1.43 +(**)end(**)