Ur/Web: demo/treeFun.urs annotate

At loop heads, havoc relations that might be changed by the loop

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 17 Apr 2010 14:26:52 -0400
parents	311ca1ae715d
children

rev	line source
adamc@469	1 functor Make(M : sig
adamc@469	2 type key
adamc@469	3 con id :: Name
adamc@469	4 con parent :: Name
adamc@469	5 con cols :: {Type}
adamc@469	6 constraint [id] ~ [parent]
adamc@469	7 constraint [id, parent] ~ cols
adamc@469	8
adamc@723	9 val key_inj : sql_injectable_prim key
adamc@469	10
adamc@706	11 table tab : ([id = key, parent = option key] ++ cols)
adamc@469	12 end) : sig
adamc@469	13
adamc@469	14 con id = M.id
adamc@469	15 con parent = M.parent
adamc@469	16
adamc@469	17 val tree : ($([id = M.key, parent = option M.key] ++ M.cols) -> xbody)
adamc@469	18 -> option M.key
adamc@469	19 -> transaction xbody
adamc@469	20
adamc@469	21 end

Mercurial > urweb