clasohm@0: (* Title: library clasohm@0: ID: $Id$ clasohm@0: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright 1992 University of Cambridge clasohm@0: clasohm@0: Basic library: booleans, lists, pairs, input/output, etc. clasohm@0: *) clasohm@0: clasohm@0: clasohm@0: (**** Booleans: operators for combining predicates ****) clasohm@0: clasohm@0: infix orf; clasohm@0: fun p orf q = fn x => p x orelse q x ; clasohm@0: clasohm@0: infix andf; clasohm@0: fun p andf q = fn x => p x andalso q x ; clasohm@0: clasohm@0: fun notf p x = not (p x) ; clasohm@0: clasohm@0: fun orl [] = false clasohm@0: | orl (x::l) = x orelse orl l; clasohm@0: clasohm@0: fun andl [] = true clasohm@0: | andl (x::l) = x andalso andl l; clasohm@0: clasohm@0: (*exists pred [x1,...,xn] ======> pred(x1) orelse ... orelse pred(xn)*) clasohm@0: fun exists (pred: 'a -> bool) : 'a list -> bool = clasohm@0: let fun boolf [] = false clasohm@0: | boolf (x::l) = (pred x) orelse boolf l clasohm@0: in boolf end; clasohm@0: clasohm@0: (*forall pred [x1,...,xn] ======> pred(x1) andalso ... andalso pred(xn)*) clasohm@0: fun forall (pred: 'a -> bool) : 'a list -> bool = clasohm@0: let fun boolf [] = true clasohm@0: | boolf (x::l) = (pred x) andalso (boolf l) clasohm@0: in boolf end; clasohm@0: clasohm@0: clasohm@0: (*** Lists ***) clasohm@0: clasohm@0: exception LIST of string; clasohm@0: clasohm@0: (*discriminator and selectors for lists. *) clasohm@0: fun null [] = true clasohm@0: | null (_::_) = false; clasohm@0: clasohm@0: fun hd [] = raise LIST "hd" clasohm@0: | hd (a::_) = a; clasohm@0: clasohm@0: fun tl [] = raise LIST "tl" clasohm@0: | tl (_::l) = l; clasohm@0: clasohm@0: clasohm@0: (*curried functions for pairing and reversed pairing*) clasohm@0: fun pair x y = (x,y); clasohm@0: fun rpair x y = (y,x); clasohm@0: clasohm@0: fun fst(x,y) = x and snd(x,y) = y; clasohm@0: clasohm@0: (*Handy combinators*) clasohm@0: fun curry f x y = f(x,y); clasohm@0: fun uncurry f(x,y) = f x y; clasohm@0: fun I x = x and K x y = x; clasohm@0: clasohm@0: (*Combine two functions forming the union of their domains*) clasohm@0: infix orelf; clasohm@0: fun f orelf g = fn x => f x handle Match=> g x; clasohm@0: clasohm@0: clasohm@0: (*Application of (infix) operator to its left or right argument*) clasohm@0: fun apl (x,f) y = f(x,y); clasohm@0: fun apr (f,y) x = f(x,y); clasohm@0: clasohm@0: clasohm@0: (*functional for pairs*) clasohm@0: fun pairself f (x,y) = (f x, f y); clasohm@0: clasohm@0: (*Apply the function to a component of a pair*) clasohm@0: fun apfst f (x, y) = (f x, y); clasohm@0: fun apsnd f (x, y) = (x, f y); clasohm@0: clasohm@0: fun square (n: int) = n*n; clasohm@0: clasohm@0: fun fact 0 = 1 clasohm@0: | fact n = n * fact(n-1); clasohm@0: clasohm@0: clasohm@0: (*The following versions of fold are designed to fit nicely with infixes.*) clasohm@0: clasohm@0: (* (op @) (e, [x1,...,xn]) ======> ((e @ x1) @ x2) ... @ xn clasohm@0: for operators that associate to the left. TAIL RECURSIVE*) clasohm@0: fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = clasohm@0: let fun itl (e, []) = e clasohm@0: | itl (e, a::l) = itl (f(e,a), l) clasohm@0: in itl end; clasohm@0: clasohm@0: (* (op @) ([x1,...,xn], e) ======> x1 @ (x2 ... @ (xn @ e)) clasohm@0: for operators that associate to the right. Not tail recursive.*) clasohm@0: fun foldr f (l,e) = clasohm@0: let fun itr [] = e clasohm@0: | itr (a::l) = f(a, itr l) clasohm@0: in itr l end; clasohm@0: clasohm@0: (* (op @) [x1,...,xn] ======> x1 @ (x2 ..(x[n-1]. @ xn)) clasohm@0: for n>0, operators that associate to the right. Not tail recursive.*) clasohm@0: fun foldr1 f l = clasohm@0: let fun itr [x] = x clasohm@0: | itr (x::l) = f(x, itr l) clasohm@0: in itr l end; clasohm@0: clasohm@0: clasohm@0: (*Length of a list. Should unquestionably be a standard function*) clasohm@0: local fun length1 (n, [ ]) = n (*TAIL RECURSIVE*) clasohm@0: | length1 (n, x::l) = length1 (n+1, l) clasohm@0: in fun length l = length1 (0,l) end; clasohm@0: clasohm@0: clasohm@0: (*Take the first n elements from l.*) clasohm@0: fun take (n, []) = [] clasohm@0: | take (n, x::xs) = if n>0 then x::take(n-1,xs) clasohm@0: else []; clasohm@0: clasohm@0: (*Drop the first n elements from l.*) clasohm@0: fun drop (_, []) = [] clasohm@0: | drop (n, x::xs) = if n>0 then drop (n-1, xs) clasohm@0: else x::xs; clasohm@0: clasohm@0: (*Return nth element of l, where 0 designates the first element; clasohm@0: raise EXCEPTION if list too short.*) clasohm@0: fun nth_elem NL = case (drop NL) of clasohm@0: [] => raise LIST "nth_elem" clasohm@0: | x::l => x; clasohm@0: clasohm@0: clasohm@0: (*make the list [from, from+1, ..., to]*) clasohm@0: infix upto; clasohm@0: fun from upto to = clasohm@0: if from>to then [] else from :: ((from+1) upto to); clasohm@0: clasohm@0: (*make the list [from, from-1, ..., to]*) clasohm@0: infix downto; clasohm@0: fun from downto to = clasohm@0: if from is = [n,n-1,...,0] *) clasohm@0: fun downto0(i::is,n) = i=n andalso downto0(is,n-1) clasohm@0: | downto0([],n) = n = ~1; clasohm@0: clasohm@0: (*Like Lisp's MAPC -- seq proc [x1,...,xn] evaluates clasohm@0: proc(x1); ... ; proc(xn) for side effects.*) clasohm@0: fun seq (proc: 'a -> unit) : 'a list -> unit = clasohm@0: let fun seqf [] = () clasohm@0: | seqf (x::l) = (proc x; seqf l) clasohm@0: in seqf end; clasohm@0: clasohm@0: clasohm@0: (*** Balanced folding; access to balanced trees ***) clasohm@0: clasohm@0: exception Balance; (*indicates non-positive argument to balancing fun*) clasohm@0: clasohm@0: (*Balanced folding; avoids deep nesting*) clasohm@0: fun fold_bal f [x] = x clasohm@0: | fold_bal f [] = raise Balance clasohm@0: | fold_bal f xs = clasohm@0: let val k = length xs div 2 clasohm@0: in f (fold_bal f (take(k,xs)), clasohm@0: fold_bal f (drop(k,xs))) clasohm@0: end; clasohm@0: clasohm@0: (*Construct something of the form f(...g(...(x)...)) for balanced access*) clasohm@0: fun access_bal (f,g,x) n i = clasohm@0: let fun acc n i = (* 1<=i<=n*) clasohm@0: if n=1 then x else clasohm@0: let val n2 = n div 2 clasohm@0: in if i<=n2 then f (acc n2 i) clasohm@0: else g (acc (n-n2) (i-n2)) clasohm@0: end clasohm@0: in if 1<=i andalso i<=n then acc n i else raise Balance end; clasohm@0: clasohm@0: (*Construct ALL such accesses; could try harder to share recursive calls!*) clasohm@0: fun accesses_bal (f,g,x) n = clasohm@0: let fun acc n = clasohm@0: if n=1 then [x] else clasohm@0: let val n2 = n div 2 clasohm@0: val acc2 = acc n2 clasohm@0: in if n-n2=n2 then map f acc2 @ map g acc2 clasohm@0: else map f acc2 @ map g (acc (n-n2)) end clasohm@0: in if 1<=n then acc n else raise Balance end; clasohm@0: clasohm@0: clasohm@0: (*** Input/Output ***) clasohm@0: clasohm@0: fun prs s = output(std_out,s); clasohm@0: fun writeln s = prs (s ^ "\n"); clasohm@0: clasohm@0: (*Print error message and abort to top level*) clasohm@0: exception ERROR; clasohm@0: fun error (msg) = (writeln msg; raise ERROR); clasohm@0: clasohm@0: fun assert p msg = if p then () else error msg; clasohm@0: fun deny p msg = if p then error msg else (); clasohm@0: clasohm@0: (*For the "test" target in Makefiles -- signifies successful termination*) clasohm@0: fun maketest msg = clasohm@0: (writeln msg; clasohm@0: output(open_out "test", "Test examples ran successfully\n")); clasohm@0: clasohm@0: (*print a list surrounded by the brackets lpar and rpar, with comma separator clasohm@0: print nothing for empty list*) clasohm@0: fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) = clasohm@0: let fun prec(x) = (prs","; pre(x)) clasohm@0: in case l of clasohm@0: [] => () clasohm@0: | x::l => (prs lpar; pre x; seq prec l; prs rpar) clasohm@0: end; clasohm@0: clasohm@0: (*print a list of items separated by newlines*) clasohm@0: fun print_list_ln (pre: 'a -> unit) : 'a list -> unit = clasohm@0: seq (fn x => (pre x; writeln"")); clasohm@0: clasohm@0: fun is_letter ch = clasohm@0: (ord"A" <= ord ch) andalso (ord ch <= ord"Z") orelse clasohm@0: (ord"a" <= ord ch) andalso (ord ch <= ord"z"); clasohm@0: clasohm@0: fun is_digit ch = clasohm@0: (ord"0" <= ord ch) andalso (ord ch <= ord"9"); clasohm@0: clasohm@0: (*letter or _ or prime (') *) clasohm@0: fun is_quasi_letter "_" = true clasohm@0: | is_quasi_letter "'" = true clasohm@0: | is_quasi_letter ch = is_letter ch; clasohm@0: clasohm@0: (*white space: blanks, tabs, newlines*) clasohm@0: val is_blank : string -> bool = fn clasohm@0: " " => true | "\t" => true | "\n" => true | _ => false; clasohm@0: clasohm@0: val is_letdig = is_quasi_letter orf is_digit; clasohm@0: clasohm@0: val to_lower = clasohm@0: let clasohm@0: fun lower ch = clasohm@0: if ch >= "A" andalso ch <= "Z" then clasohm@0: chr (ord ch - ord "A" + ord "a") clasohm@0: else ch; clasohm@0: in clasohm@0: implode o (map lower) o explode clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: (*** Timing ***) clasohm@0: clasohm@0: (*Unconditional timing function*) clasohm@0: val timeit = cond_timeit true; clasohm@0: clasohm@0: (*Timed application function*) clasohm@0: fun timeap f x = timeit(fn()=> f x); clasohm@0: clasohm@0: (*Timed "use" function, printing filenames*) clasohm@0: fun time_use fname = timeit(fn()=> clasohm@0: (writeln("\n**** Starting " ^ fname ^ " ****"); use fname; clasohm@0: writeln("\n**** Finished " ^ fname ^ " ****"))); clasohm@0: clasohm@0: clasohm@0: (*** Misc functions ***) clasohm@0: clasohm@0: (*Function exponentiation: f(...(f x)...) with n applications of f *) clasohm@0: fun funpow n f x = clasohm@0: let fun rep (0,x) = x clasohm@0: | rep (n,x) = rep (n-1, f x) clasohm@0: in rep (n,x) end; clasohm@0: clasohm@0: (*Combine two lists forming a list of pairs: clasohm@0: [x1,...,xn] ~~ [y1,...,yn] ======> [(x1,y1), ..., (xn,yn)] *) clasohm@0: infix ~~; clasohm@0: fun [] ~~ [] = [] clasohm@0: | (x::xs) ~~ (y::ys) = (x,y) :: (xs ~~ ys) clasohm@0: | _ ~~ _ = raise LIST "~~"; clasohm@0: clasohm@0: (*Inverse of ~~; the old 'split'. clasohm@0: [(x1,y1), ..., (xn,yn)] ======> ( [x1,...,xn] , [y1,...,yn] ) *) clasohm@0: fun split_list (l: ('a*'b)list) = (map #1 l, map #2 l); clasohm@0: clasohm@0: (*make the list [x; x; ...; x] of length n*) clasohm@0: fun replicate n (x: 'a) : 'a list = clasohm@0: let fun rep (0,xs) = xs clasohm@0: | rep (n,xs) = rep(n-1, x::xs) clasohm@0: in if n<0 then raise LIST "replicate" clasohm@0: else rep (n,[]) clasohm@0: end; clasohm@0: clasohm@0: (*Flatten a list of lists to a list.*) clasohm@0: fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls,[]); clasohm@0: clasohm@0: clasohm@0: (*** polymorphic set operations ***) clasohm@0: clasohm@0: (*membership in a list*) clasohm@0: infix mem; clasohm@0: fun x mem [] = false clasohm@0: | x mem (y::l) = (x=y) orelse (x mem l); clasohm@0: clasohm@0: (*insertion into list if not already there*) clasohm@0: infix ins; clasohm@0: fun x ins xs = if x mem xs then xs else x::xs; clasohm@0: clasohm@0: (*union of sets represented as lists: no repetitions*) clasohm@0: infix union; clasohm@0: fun xs union [] = xs clasohm@0: | [] union ys = ys clasohm@0: | (x::xs) union ys = xs union (x ins ys); clasohm@0: clasohm@0: infix inter; clasohm@0: fun [] inter ys = [] clasohm@0: | (x::xs) inter ys = if x mem ys then x::(xs inter ys) clasohm@0: else xs inter ys; clasohm@0: clasohm@0: infix subset; clasohm@0: fun [] subset ys = true clasohm@0: | (x::xs) subset ys = x mem ys andalso xs subset ys; clasohm@0: clasohm@0: (*removing an element from a list WITHOUT duplicates*) clasohm@0: infix \; clasohm@0: fun (y::ys) \ x = if x=y then ys else y::(ys \ x) clasohm@0: | [] \ x = []; clasohm@0: clasohm@0: infix \\; clasohm@0: val op \\ = foldl (op \); clasohm@0: clasohm@0: (*** option stuff ***) clasohm@0: clasohm@0: datatype 'a option = None | Some of 'a; clasohm@0: clasohm@0: exception OPTION of string; clasohm@0: clasohm@0: fun the (Some x) = x clasohm@0: | the None = raise OPTION "the"; clasohm@0: clasohm@0: fun is_some (Some _) = true clasohm@0: | is_some None = false; clasohm@0: clasohm@0: fun is_none (Some _) = false clasohm@0: | is_none None = true; clasohm@0: clasohm@0: clasohm@0: (*** Association lists ***) clasohm@0: clasohm@0: (*Association list lookup*) clasohm@0: fun assoc ([], key) = None clasohm@0: | assoc ((keyi,xi)::pairs, key) = clasohm@0: if key=keyi then Some xi else assoc (pairs,key); clasohm@0: clasohm@0: fun assocs ps x = case assoc(ps,x) of None => [] | Some(ys) => ys; clasohm@0: clasohm@0: (*Association list update*) clasohm@0: fun overwrite(al,p as (key,_)) = clasohm@0: let fun over((q as (keyi,_))::pairs) = clasohm@0: if keyi=key then p::pairs else q::(over pairs) clasohm@0: | over[] = [p] clasohm@0: in over al end; clasohm@0: clasohm@0: (*Copy the list preserving elements that satisfy the predicate*) clasohm@0: fun filter (pred: 'a->bool) : 'a list -> 'a list = clasohm@0: let fun filt [] = [] clasohm@0: | filt (x::xs) = if pred(x) then x :: filt xs else filt xs clasohm@0: in filt end; clasohm@0: clasohm@0: fun filter_out f = filter (not o f); clasohm@0: clasohm@0: clasohm@0: (*** List operations, generalized to an arbitrary equality function "eq" clasohm@0: -- so what good are equality types?? ***) clasohm@0: clasohm@0: (*removing an element from a list -- possibly WITH duplicates*) clasohm@0: fun gen_rem eq (xs,y) = filter_out (fn x => eq(x,y)) xs; clasohm@0: clasohm@0: (*generalized membership test*) clasohm@0: fun gen_mem eq (x, []) = false clasohm@0: | gen_mem eq (x, y::ys) = eq(x,y) orelse gen_mem eq (x,ys); clasohm@0: clasohm@0: (*generalized insertion*) clasohm@0: fun gen_ins eq (x,xs) = if gen_mem eq (x,xs) then xs else x::xs; clasohm@0: clasohm@0: (*generalized union*) clasohm@0: fun gen_union eq (xs,[]) = xs clasohm@0: | gen_union eq ([],ys) = ys clasohm@0: | gen_union eq (x::xs,ys) = gen_union eq (xs, gen_ins eq (x,ys)); clasohm@0: clasohm@0: (*Generalized association list lookup*) clasohm@0: fun gen_assoc eq ([], key) = None clasohm@0: | gen_assoc eq ((keyi,xi)::pairs, key) = clasohm@0: if eq(key,keyi) then Some xi else gen_assoc eq (pairs,key); clasohm@0: clasohm@0: (** Finding list elements and duplicates **) clasohm@0: clasohm@0: (* find the position of an element in a list *) clasohm@0: fun find(x,ys) = clasohm@0: let fun f(y::ys,i) = if x=y then i else f(ys,i+1) clasohm@0: | f(_,_) = raise LIST "find" clasohm@0: in f(ys,0) end; clasohm@0: clasohm@0: (*Returns the tail beginning with the first repeated element, or []. *) clasohm@0: fun findrep [] = [] clasohm@0: | findrep (x::xs) = if x mem xs then x::xs else findrep xs; clasohm@0: clasohm@0: fun distinct1 (seen, []) = rev seen clasohm@0: | distinct1 (seen, x::xs) = clasohm@0: if x mem seen then distinct1 (seen, xs) clasohm@0: else distinct1 (x::seen, xs); clasohm@0: clasohm@0: (*Makes a list of the distinct members of the input*) clasohm@0: fun distinct xs = distinct1([],xs); clasohm@0: clasohm@0: clasohm@0: (*Use the keyfun to make a list of (x,key) pairs.*) clasohm@0: fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list = clasohm@0: let fun keypair x = (x, keyfun x) clasohm@0: in map keypair end; clasohm@0: clasohm@0: (*Given a list of (x,key) pairs and a searchkey clasohm@0: return the list of xs from each pair whose key equals searchkey*) clasohm@0: fun keyfilter [] searchkey = [] clasohm@0: | keyfilter ((x,key)::pairs) searchkey = clasohm@0: if key=searchkey then x :: keyfilter pairs searchkey clasohm@0: else keyfilter pairs searchkey; clasohm@0: clasohm@0: fun mapfilter (f: 'a -> 'b option) ([]: 'a list) = [] : 'b list clasohm@0: | mapfilter f (x::xs) = clasohm@0: case (f x) of clasohm@0: None => mapfilter f xs clasohm@0: | Some y => y :: mapfilter f xs; clasohm@0: clasohm@0: clasohm@0: (*Partition list into elements that satisfy predicate and those that don't. clasohm@0: Preserves order of elements in both lists. *) clasohm@0: fun partition (pred: 'a->bool) (ys: 'a list) : ('a list * 'a list) = clasohm@0: let fun part ([], answer) = answer clasohm@0: | part (x::xs, (ys, ns)) = if pred(x) clasohm@0: then part (xs, (x::ys, ns)) clasohm@0: else part (xs, (ys, x::ns)) clasohm@0: in part (rev ys, ([],[])) end; clasohm@0: clasohm@0: clasohm@0: fun partition_eq (eq:'a * 'a -> bool) = clasohm@0: let fun part [] = [] clasohm@0: | part (x::ys) = let val (xs,xs') = partition (apl(x,eq)) ys clasohm@0: in (x::xs)::(part xs') end clasohm@0: in part end; clasohm@0: clasohm@0: clasohm@0: (*Partition a list into buckets [ bi, b(i+1),...,bj ] clasohm@0: putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*) clasohm@0: fun partition_list p i j = clasohm@0: let fun part k xs = clasohm@0: if k>j then clasohm@0: (case xs of [] => [] clasohm@0: | _ => raise LIST "partition_list") clasohm@0: else clasohm@0: let val (ns,rest) = partition (p k) xs; clasohm@0: in ns :: part(k+1)rest end clasohm@0: in part i end; clasohm@0: clasohm@0: clasohm@0: (*Insertion sort. Stable (does not reorder equal elements) clasohm@0: 'less' is less-than test on type 'a. *) clasohm@0: fun sort (less: 'a*'a -> bool) = clasohm@0: let fun insert (x, []) = [x] clasohm@0: | insert (x, y::ys) = clasohm@0: if less(y,x) then y :: insert (x,ys) else x::y::ys; clasohm@0: fun sort1 [] = [] clasohm@0: | sort1 (x::xs) = insert (x, sort1 xs) clasohm@0: in sort1 end; clasohm@0: clasohm@0: (*Transitive Closure. Not Warshall's algorithm*) clasohm@0: fun transitive_closure [] = [] clasohm@0: | transitive_closure ((x,ys)::ps) = clasohm@0: let val qs = transitive_closure ps clasohm@0: val zs = foldl (fn (zs,y) => assocs qs y union zs) (ys,ys) clasohm@0: fun step(u,us) = (u, if x mem us then zs union us else us) clasohm@0: in (x,zs) :: map step qs end; clasohm@0: clasohm@0: (*** Converting integers to strings, generating identifiers, etc. ***) clasohm@0: clasohm@0: (*Expand the number in the given base clasohm@0: example: radixpand(2, 8) gives [1, 0, 0, 0] *) clasohm@0: fun radixpand (base,num) : int list = clasohm@0: let fun radix (n,tail) = clasohm@0: if nn then max(m::ns) else max(n::ns) clasohm@0: | max [] = raise LIST "max"; clasohm@0: clasohm@0: fun min[m : int] = m clasohm@0: | min(m::n::ns) = if m ([x1,...,x(i-1)], [xi,..., xn]) clasohm@0: where xi is the first element that does not satisfy the predicate*) clasohm@0: fun take_prefix (pred : 'a -> bool) (xs: 'a list) : 'a list * 'a list = clasohm@0: let fun take (rxs, []) = (rev rxs, []) clasohm@0: | take (rxs, x::xs) = clasohm@0: if pred x then take(x::rxs, xs) else (rev rxs, x::xs) clasohm@0: in take([],xs) end; clasohm@0: clasohm@0: infix prefix; clasohm@0: fun [] prefix _ = true clasohm@0: | (x::xs) prefix (y::ys) = (x=y) andalso (xs prefix ys) clasohm@0: | _ prefix _ = false; clasohm@0: clasohm@0: (* [x1, x2, ..., xn] ---> [x1, s, x2, s, ..., s, xn] *) clasohm@0: fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs clasohm@0: | separate _ xs = xs; clasohm@0: clasohm@0: (*space_implode "..." (explode "hello"); gives "h...e...l...l...o" *) clasohm@0: fun space_implode a bs = implode (separate a bs); clasohm@0: clasohm@0: fun quote s = "\"" ^ s ^ "\""; clasohm@0: clasohm@0: (*Concatenate messages, one per line, into a string*) clasohm@0: val cat_lines = implode o (map (apr(op^,"\n"))); clasohm@0: clasohm@0: (*Scan a list of characters into "words" composed of "letters" (recognized clasohm@0: by is_let) and separated by any number of non-"letters".*) clasohm@0: fun scanwords is_let cs = clasohm@0: let fun scan1 [] = [] clasohm@0: | scan1 cs = clasohm@0: let val (lets, rest) = take_prefix is_let cs clasohm@0: in implode lets :: scanwords is_let rest end; clasohm@0: in scan1 (#2 (take_prefix (not o is_let) cs)) end;