irc.freenode.net changed the topic of #ocaml to: OCaml 3.08 "Bastille Day" Release available ! -- Archive of Caml Weekly News: http://pauillac.inria.fr/~aschmitt/cwn , A tutorial: http://merjis.com/richj/computers/ocaml/tutorial/ , A free book: http://cristal.inria.fr/~remy/cours/appsem, Mailing List (best ml ever for any computer language): http://caml.inria.fr/bin/wilma/caml-list
sic- has quit [Read error: 60 (Operation timed out)]
Excedrin has joined #ocaml
monochrom has quit ["Don't talk to those who talk to themselves."]
Nutssh has quit ["Client exiting"]
Nutssh has joined #ocaml
Nutssh has left #ocaml []
bk_ has quit ["Leaving IRC - dircproxy 1.1.0"]
CosmicRay has joined #ocaml
vezenchio has joined #ocaml
CosmicRay has quit ["Client exiting"]
fab_ has joined #ocaml
ericc has joined #ocaml
_fab has quit [Read error: 110 (Connection timed out)]
cjohnson has quit ["Leaving"]
Xolution has joined #ocaml
mrsolo has joined #ocaml
mrsolo_ has joined #ocaml
grirgz has quit [Read error: 238 (Connection timed out)]
mrsolo has quit [Read error: 113 (No route to host)]
mrsolo_ has quit [Read error: 113 (No route to host)]
mrsolo_ has joined #ocaml
Hipo_ is now known as HIpo
HIpo is now known as Hipo
oracle1 has joined #ocaml
<oracle1> anyone used cil?
<oracle1> i wonder how to best compare two parse trees for equality or to compute the difference of two similar parse trees.
smimou has joined #ocaml
kinners has joined #ocaml
jason_ has joined #ocaml
<jason_> Hm, if I have a function defined in my program that takes a "string->unit." And another piece of code in another module that uses it, if I avoid specifying the type the code will compile 'only' if I use that piece of code in another module. If I don't use it it becomes an unbound type.
<jason_> If I don't specify types of arguments to my functions will this always be the case?
<jason_> It would be nice if my module could just be compiled, and that is that.
smimou has quit ["?"]
kinners has quit [Read error: 110 (Connection timed out)]
tea has left #ocaml []
jason_ has quit [Remote closed the connection]
grirgz has joined #ocaml
tomp has quit ["Client Exiting"]
menace has joined #ocaml
budjet has joined #ocaml
budjet has quit [Remote closed the connection]
Iter has joined #ocaml
Hadaka has quit [Read error: 60 (Operation timed out)]
Hipo has quit [Read error: 104 (Connection reset by peer)]
Hipo has joined #ocaml
<oracle1> anyone used cil?
<oracle1> i wonder how to best compare two parse trees for equality or to compute the difference of two similar parse trees.
Iter has quit [Read error: 110 (Connection timed out)]
Naked has joined #ocaml
Naked is now known as Hadaka
bk_ has joined #ocaml
pflanze has joined #ocaml
mlh has joined #ocaml
mlh has quit [Client Quit]
<Smerdyakov> oracle1, you'd probably have to implement it all yourself.
pflanze has quit [Read error: 60 (Operation timed out)]
Submarine has joined #ocaml
<oracle1> smerdyakov: yes, that's what I expected
<oracle1> still, somebody might have already The Solution (TM)
<Smerdyakov> oracle1, well, you can e-mail the authors.
<Smerdyakov> oracle1, they don't mind. I'm in that research group. :)
<oracle1> sounds good. So i could address you directly heh
<Smerdyakov> No, I only use Cil as a user. :)
<oracle1> that does not count, sorry.
<Smerdyakov> But my advisor and some of his students are the authors.
<Submarine> Smerdyakov, which research group? :-)
<Smerdyakov> Submarine, depending on the granularity level, either http://www.cs.berkeley.edu/~necula/ or http://osq.cs.berkeley.edu/ :)
<Submarine> ah, you're a student of George!
<Smerdyakov> oracle1, Jeremy and Matt are the two most junior people who worked on it.
<Smerdyakov> oracle1, so e-mail them if you want a most likely answer. :)
<Submarine> are you the guy who presented the paper at CC in Grenoble?
<Smerdyakov> No. I have not presented a paper yet. :)
<oracle1> ok thanks
<oracle1> heh
<Submarine> too bad George had his frontend written by his students AFTER we wrote our own
<Smerdyakov> Submarine, I bet CIL is better than yours, eh? :)
<Submarine> ours is a piece of crap
<Smerdyakov> Submarine, and George actually wrote some of the code, I think. :P
<oracle1> come on it's just a frontc ripp :)
<Submarine> Smerdyakov, ever had a look at www.astree.ens.fr?
<Smerdyakov> Submarine, someone pointed it out before.
<oracle1> without source, isnt it ?
<Submarine> Without source, until we sort out many problems.
<Smerdyakov> Well, I've worked on this: http://www-cad.eecs.berkeley.edu/~rupak/blast/
<Smerdyakov> I guess they might not be distributing the source, either.
<oracle1> ah, you're part of it. at least it sounds interesting
<Submarine> BLAST? Tom Henzinger's thing?
<Smerdyakov> I don't know how Astree works, but counterexample-driven predicate abstraction is a pretty cool idea that works quite well. :)
<Smerdyakov> That is right.
<Submarine> Smerdyakov, if Patrick Cousot was around, he'd give you examples of where it does not work.
<Smerdyakov> OK, but it's a nice way of thinking about lots of things.
<Submarine> Astree is a 'conventional' forward-only abstract interpreter based on denotational semantics.
<Submarine> it has naive notions of memory and pointers
<Submarine> a very fast interval analysis
<Submarine> and a bunch of specialized domains
<Submarine> and a ton of extra tricks
<Smerdyakov> BLAST uses a very general framework within the model checker and relies on a theorem prover to do the specialized stuff.
<Submarine> I know. You use SIMPLIFY. :-)
<Smerdyakov> There are other theorem provers that you can use, as well.
<Submarine> I actually saw Henzinger one week ago explaining how you looked for the cut in the contradiction.
<Smerdyakov> Yeah. That depends on using the Foci theorem prover.
<Smerdyakov> Which applies that model theoretic result whose name I forget now.
<Smerdyakov> Ah. "Craig's interpolation theorem."
<Submarine> exactly
<Submarine> still, it's some of a mystery to me how you choose the predicate to use
<Smerdyakov> It's easy, I think.
<Smerdyakov> You ask the theorem prover to prove that the supposed error trace you've found in invalid.
<Smerdyakov> If it proves it, you add every predicate found in the proof.
<Submarine> and the "focus" thing just restricts to the predicates used for the proof that the "cut" is false
<Smerdyakov> It restricts the part of the proof that are relevant to each program point found in the trace, yes.
* Smerdyakov leaves for a bit.
<oracle1> i would like to have a generic function which returns the argument of a constructor
<Submarine> eeew?
<oracle1> but that's probably not possible like i want it..
<Smerdyakov> oracle1, it's hard to tell why you want that, but the usual way to avoid inconveniences associated with such things is to write a fold function over your custom data type.
<Submarine> I don't understand what oracle1 wants.
<oracle1> e.g. when I give the function this as argument: CallA(CallB(CallA(A(10))))
<oracle1> it should return CallB(CallA(A(10))).
<Submarine> oooh
<Submarine> it's plain old pattern matching
<oracle1> this works fine as long as the argument of the constructor is of the same type
bk_ has quit [Remote closed the connection]
bk_ has joined #ocaml
<Submarine> ?!?
<oracle1> well given these two types
<oracle1> type a = A of int | CallB of b | Empty
<oracle1> and b = B of int | CallA of a
<oracle1> how would you write a function next_b which returns the next argument of a b type ?
<oracle1> but maybe I have the wrong problems heh..or I have to do it differently in ocaml
<Submarine> oracle1, you have the wrong problems
<Submarine> or you *might* use polymorphic variants
<oracle1> no, I can't change the existing types
<pnou> Submarine: polymorphic variants won't change anything
<Submarine> pnou, he could stuff everything into a single type for the purpose of this function
<pnou> this would do almost the same thing as the identity :)
<Submarine> (yes)
vezenchio has quit ["Hydrocon technology produces two waste products: steam and green goo. We dispose of the steam through various vents, strategic"]
Submarine has quit ["ChatZilla 0.8.31 [Mozilla rv:1.4.1/20031114]"]
menace has quit []
Riastrad1 has joined #ocaml
Riastradh has quit [Nick collision from services.]
Riastrad1 is now known as Riastradh
Xolution has quit [Read error: 54 (Connection reset by peer)]
Xolution has joined #ocaml
maihem has joined #ocaml
budjet has joined #ocaml
budjet has quit [Connection reset by peer]
budjet has joined #ocaml
<Hadaka> what's the perfect and cleanest way to print a list of values with commas between the values?
<Smerdyakov> You can use String.concat for part of the work.
<Hadaka> um, yeah I just need printing
<Hadaka> can I somehow match a list which has atleast two elements?
<mflux> match list with a::b::_ -> ..
<mflux> parsed as a::(b::_), so no special syntax there
<Hadaka> right
buddjett has joined #ocaml
budjet has quit [Success]
buddjett has quit [Read error: 104 (Connection reset by peer)]
budjet has joined #ocaml
budjet has quit [Read error: 54 (Connection reset by peer)]