1.1 --- a/src/Tools/isac/Specify/o-model.sml Mon Jun 20 18:43:51 2022 +0200
1.2 +++ b/src/Tools/isac/Specify/o-model.sml Tue Jun 21 12:41:52 2022 +0200
1.3 @@ -45,27 +45,23 @@
1.4 type preori
1.5 val copy_name: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
1.6 val is_copy_named: Model_Pattern.single -> bool
1.7 - val is_copy_named_idstr: string -> bool
1.8 + val is_copy_named': string -> bool
1.9 val is_copy_named_generating: Model_Pattern.single -> bool
1.10
1.11 val get_field_term: theory -> single -> m_field * UnparseC.term_as_string
1.12
1.13 \<^isac_test>\<open>
1.14 val is_copy_named_generating_idstr: string -> bool
1.15 - val preoris2str : preori list -> string
1.16 + val string_of_preoris : preori list -> string
1.17 val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
1.18 +
1.19 val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
1.20 -(*/------- rename -------\*)
1.21 -(*val max_variant: variants -> int*)
1.22 - val max: variants -> int
1.23 -(*val coll_variants: ('a * ''b) list -> ('a list * ''b) list*)
1.24 - val coll_variants: ('a * ''b) list -> ('a list * ''b) list
1.25 -(*val replace_0: int -> int list -> int list*)
1.26 + val max_variant: variants -> int
1.27 + val partition_variants: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
1.28 + val collect_variants: ('a * ''b) list -> ('a list * ''b) list
1.29 +
1.30 val replace_0: int -> int list -> int list
1.31 val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
1.32 -(*val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list*)
1.33 - val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
1.34 -(*\------- rename -------/*)
1.35 \<close>
1.36 end
1.37
1.38 @@ -96,7 +92,7 @@
1.39 fun preori2str (vs, fi, t, ts) =
1.40 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
1.41 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
1.42 -val preoris2str = (strs2str' o (map (linefeed o preori2str)));
1.43 +val string_of_preoris = (strs2str' o (map (linefeed o preori2str)));
1.44 \<close>
1.45
1.46 (* get the first term in ts from ori *)
1.47 @@ -119,13 +115,13 @@
1.48 mark an element with the position within a plateau;
1.49 a plateau with length 1 is marked with 0
1.50 *)
1.51 -fun mark _ [] = raise ERROR "mark []"
1.52 - | mark eq xs =
1.53 +fun partition_variants _ [] = raise ERROR "partition_variants []"
1.54 + | partition_variants eq xs =
1.55 let
1.56 fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
1.57 - | mar _ _ [] _ = raise ERROR "mark []"
1.58 - | mar xx eq (x:: x' :: xs) n =
1.59 - if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
1.60 + | mar _ _ [] _ = raise ERROR "partition_variants []"
1.61 + | mar xx eq (x :: x' :: xs) n =
1.62 + if eq (x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
1.63 else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
1.64 in mar [] eq xs 1 end;
1.65
1.66 @@ -137,22 +133,22 @@
1.67 fun add_variants fdts =
1.68 let
1.69 fun eq (a, b) = curry op= (snd3 a) (snd3 b);
1.70 - in mark eq fdts end;
1.71 + in partition_variants eq fdts end;
1.72
1.73 -fun max [] = raise ERROR "max of []"
1.74 - | max (y :: ys) =
1.75 +fun max_variant [] = raise ERROR "max_variant of []"
1.76 + | max_variant (y :: ys) =
1.77 let fun mx x [] = x
1.78 | mx x (y :: ys) = if x < y then mx y ys else mx x ys;
1.79 in mx y ys end;
1.80
1.81 -fun coll_variants (((v,x) :: vxs)) =
1.82 +fun collect_variants (((v,x) :: vxs)) =
1.83 let
1.84 fun col xs (vs, x) [] = xs @ [(vs, x)]
1.85 | col xs (vs, x) ((v', x') :: vxs') =
1.86 if x = x' then col xs (vs @ [v'], x') vxs'
1.87 else col (xs @ [(vs, x)]) ([v'], x') vxs';
1.88 in col [] ([v], x) vxs end
1.89 - | coll_variants _ = raise ERROR "coll_variants: called with []";
1.90 + | collect_variants _ = raise ERROR "collect_variants: called with []";
1.91
1.92 fun replace_0 vm [0] = intsto vm
1.93 | replace_0 _ vs = vs;
1.94 @@ -175,10 +171,10 @@
1.95 |> Input_Descript.split
1.96 |> add_field thy pbt) fmz)
1.97 |> add_variants;
1.98 - val maxv = model |> map fst |> max;
1.99 + val maxv = model |> map fst |> max_variant;
1.100 val maxv = if maxv = 0 then 1 else maxv;
1.101 val model' = model
1.102 - |> coll_variants
1.103 + |> collect_variants
1.104 |> map (replace_0 maxv |> apfst)
1.105 |> add_enumerate
1.106 |> map flattup;
1.107 @@ -192,7 +188,7 @@
1.108 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
1.109 fun mkval' x = mkval TermC.empty x;
1.110 (* from an O_Model create values for ctxt *)
1.111 -fun values (oris:T) =
1.112 +fun values oris =
1.113 ((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris
1.114
1.115 (* from an O_Model create (Formalise.model, values)
1.116 @@ -236,15 +232,15 @@
1.117 (* make oris from args of the stac SubProblem and from pbt.
1.118 can this formal argument (of a model-pattern) be omitted in the arg-list
1.119 of a SubProblem ? see calcelems.sml 'type met ' *)
1.120 -fun is_copy_named_idstr str =
1.121 +fun is_copy_named' str =
1.122 case (rev o Symbol.explode) str of
1.123 "'" :: _ :: "'" :: _ => true
1.124 | _ => false
1.125 -fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
1.126 +fun is_copy_named (_, (_, t)) = (is_copy_named' o TermC.free2str) t
1.127
1.128 (* should this formal argument (of a model-pattern) create a new identifier? *)
1.129 fun is_copy_named_generating_idstr str =
1.130 - if is_copy_named_idstr str
1.131 + if is_copy_named' str
1.132 then
1.133 case (rev o Symbol.explode) str of
1.134 "'" :: "'" :: "'" :: _ => false