clarified signature;
authorwenzelm
Sun Jan 28 16:09:00 2018 +0100 (18 months ago)
changeset 675216a27e86cc2e7
parent 67520 6ff47e27c32d
child 67522 9e712280cc37
clarified signature;
src/Pure/library.ML
src/Tools/Code/code_namespace.ML
     1.1 --- a/src/Pure/library.ML	Sun Jan 28 12:57:35 2018 +0100
     1.2 +++ b/src/Pure/library.ML	Sun Jan 28 16:09:00 2018 +0100
     1.3 @@ -101,8 +101,8 @@
     1.4    val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
     1.5    val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
     1.6    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
     1.7 -  val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
     1.8    val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
     1.9 +  val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
    1.10    val prefixes1: 'a list -> 'a list list
    1.11    val prefixes: 'a list -> 'a list list
    1.12    val suffixes1: 'a list -> 'a list list
    1.13 @@ -540,14 +540,6 @@
    1.14              if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
    1.15    in  take([], xs)  end;
    1.16  
    1.17 -fun chop_prefix eq ([], ys) = ([], ([], ys))
    1.18 -  | chop_prefix eq (xs, []) = ([], (xs, []))
    1.19 -  | chop_prefix eq (xs as x :: xs', ys as y :: ys') =
    1.20 -      if eq (x, y) then
    1.21 -        let val (ps', xys'') = chop_prefix eq (xs', ys')
    1.22 -        in (x :: ps', xys'') end
    1.23 -      else ([], (xs, ys));
    1.24 -
    1.25  (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
    1.26     where xi is the last element that does not satisfy the predicate*)
    1.27  fun take_suffix _ [] = ([], [])
    1.28 @@ -556,6 +548,14 @@
    1.29          ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
    1.30        | (prfx, sffx) => (x :: prfx, sffx));
    1.31  
    1.32 +fun chop_common_prefix eq ([], ys) = ([], ([], ys))
    1.33 +  | chop_common_prefix eq (xs, []) = ([], (xs, []))
    1.34 +  | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') =
    1.35 +      if eq (x, y) then
    1.36 +        let val (ps', xys'') = chop_common_prefix eq (xs', ys')
    1.37 +        in (x :: ps', xys'') end
    1.38 +      else ([], (xs, ys));
    1.39 +
    1.40  fun prefixes1 [] = []
    1.41    | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
    1.42  
     2.1 --- a/src/Tools/Code/code_namespace.ML	Sun Jan 28 12:57:35 2018 +0100
     2.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Jan 28 16:09:00 2018 +0100
     2.3 @@ -382,7 +382,7 @@
     2.4          val (name_fragments, _) = prep_sym sym;
     2.5          val (name_fragments', _) = prep_sym sym';
     2.6          val (name_fragments_common, (diff, diff')) =
     2.7 -          chop_prefix (op =) (name_fragments, name_fragments');
     2.8 +          chop_common_prefix (op =) (name_fragments, name_fragments');
     2.9          val is_cross_module = not (null diff andalso null diff');
    2.10          val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
    2.11          val add_edge = if is_cross_module andalso not cyclic_modules
    2.12 @@ -432,7 +432,7 @@
    2.13      fun deresolver prefix_fragments sym =
    2.14        let
    2.15          val (name_fragments, _) = prep_sym sym;
    2.16 -        val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
    2.17 +        val (_, (_, remainder)) = chop_common_prefix (op =) (prefix_fragments, name_fragments);
    2.18          val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
    2.19           of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
    2.20          val (base', _) = Code_Symbol.Graph.get_node nodes sym;