Ur/Web: tests/constraint.ur annotate

annotate tests/constraint.ur @ 416:679b2fbbd4d0

Counter demo

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 23 Oct 2008 11:59:48 -0400
parents	71bafe66dbe1
children

rev	line source
adamc@88	1 signature S = sig
adamc@88	2 con nm :: Name
adamc@88	3 con r :: {Type}
adamc@88	4
adamc@88	5 constraint [nm] ~ r
adamc@88	6 end
adamc@88	7
adamc@88	8 structure M : S = struct
adamc@88	9 con nm = #A
adamc@88	10 con r = [B = float, C = string]
adamc@88	11
adamc@88	12 constraint [A] ~ [B]
adamc@88	13 constraint [nm] ~ r
adamc@88	14 constraint [C] ~ [D]
adamc@88	15 end
adamc@88	16
adamc@88	17 structure M' = struct
adamc@88	18 open M
adamc@88	19
adamc@88	20 con combo = [nm = int] ++ r
adamc@88	21 end
adamc@88	22
adamc@88	23 structure M' = struct
adamc@88	24 open constraints M
adamc@88	25
adamc@88	26 con nm' = M.nm
adamc@88	27 con r' = M.r
adamc@88	28 con combo = [nm' = int] ++ r'
adamc@88	29 end
adamc@89	30
adamc@89	31
adamc@89	32 signature S' = sig
adamc@89	33 con r1 :: {Type}
adamc@89	34 con r2 :: {Type}
adamc@89	35
adamc@89	36 constraint r1 ~ r2
adamc@89	37 end
adamc@89	38
adamc@89	39 functor F (M : S) : S' = struct
adamc@89	40 con r1 = [M.nm = int]
adamc@89	41 con r2 = M.r
adamc@89	42
adamc@89	43 open constraints M
adamc@89	44 constraint r1 ~ r2
adamc@89	45 end