# HG changeset patch # User haftmann # Date 1135064290 -3600 # Node ID 7488d8ea61bcdf5f83ef99e5bba048d5b739866e # Parent 72ee07f4b56b77a4cba81ed19826656f922e8ccf removed infix prefix, introduces burrow diff -r 72ee07f4b56b -r 7488d8ea61bc src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Dec 20 04:29:25 2005 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Dec 20 08:38:10 2005 +0100 @@ -1239,7 +1239,7 @@ let val _ = writeln "TRANSFORMING FUN (1)"; val varnames_ctxt = - dig + burrow (Term.invent_names ((vars_of_iexprs o map snd) eqs @ (vars_of_ipats o Library.flat o map fst) eqs) "d" o length) (map snd sortctxt); diff -r 72ee07f4b56b -r 7488d8ea61bc src/Pure/library.ML --- a/src/Pure/library.ML Tue Dec 20 04:29:25 2005 +0100 +++ b/src/Pure/library.ML Tue Dec 20 08:38:10 2005 +0100 @@ -13,7 +13,7 @@ infix 3 o oo ooo oooo; infix 4 ~~ upto downto; -infix orf andf prefix \ \\ ins ins_string ins_int mem mem_int mem_string union union_int +infix orf andf \ \\ ins ins_string ins_int mem mem_int mem_string union union_int union_string inter inter_int inter_string subset subset_int subset_string; signature BASIC_LIBRARY = @@ -101,7 +101,7 @@ val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list - val dig: ('a list -> 'a list) -> 'a list list -> 'a list list + val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list val unflat: 'a list list -> 'b list -> 'b list list val splitAt: int * 'a list -> 'a list * 'a list val dropwhile: ('a -> bool) -> 'a list -> 'a list @@ -125,7 +125,7 @@ val filter: ('a -> bool) -> 'a list -> 'a list val filter_out: ('a -> bool) -> 'a list -> 'a list val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool - val prefix: ''a list * ''a list -> bool + val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list val prefixes1: 'a list -> 'a list list @@ -596,7 +596,7 @@ | unflat [] [] = [] | unflat _ _ = raise UnequalLengths; -fun dig f xss = +fun burrow f xss = unflat xss ((f o flat) xss); @@ -672,9 +672,9 @@ (* prefixes, suffixes *) -fun [] prefix _ = true - | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys) - | _ prefix _ = false; +fun is_prefix _ [] _ = true + | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys + | is_prefix eq _ _ = false; (* [x1, ..., xi, ..., xn] ---> ([x1, ..., x(i-1)], [xi, ..., xn]) where xi is the first element that does not satisfy the predicate*)