000001| (** Abstract string datatype and operations *)
000002|
000003| type elem =
000004| | Bot
000005| | Const of string
000006| | Top
000007|
000008| (* eq : elem -> elem -> bool *)
000009| let eq (a:elem) a' = (*[2]*)a = a'
000010|
000011| (* leq : elem -> elem -> bool *)
000012| let leq s s' = match s,s' with
000013| | Bot,_ -> (*[402765]*)true
000014| | _,Bot -> (*[3789]*)false
000015| | _,Top -> (*[13841]*)true
000016| | Top,_ -> (*[14]*)false
000017| | Const c, Const c' -> (*[5101]*)c=c'
000018|
000019| (* join : elem -> elem -> elem *)
000020| let join s s' = match s,s' with
000021| | Bot,_ -> (*[6237206]*)s'
000022| | _,Bot -> (*[1604]*)s
000023| | Top,_ -> (*[220480]*)Top
000024| | _,Top -> (*[230]*)Top
000025| | Const c, Const c' -> (*[91310]*)if c=c' then (*[91243]*)s else (*[67]*)Top
000026|
000027| (* meet : elem -> elem -> elem *)
000028| let meet s s' = match s,s' with
000029| | Bot,_ -> (*[442]*)Bot
000030| | _,Bot -> (*[33]*)Bot
000034|
000035| (* const : string -> elem *)
000036| let const s = (*[2882]*)Const s
000037|
000038| (* bot : elem *)
000039| let bot = (*[1]*)Bot
000040|
000041| (* top : elem *)
000042| let top = (*[1]*)Top
000043|
000044| (* upper : elem -> elem *)
000045| let upper s = match s with
000054| | Const c -> (*[2]*)Const (String.lowercase c)
000055|
000056| (* concat : elem -> elem -> elem *)
000057| let concat s s' = match s,s' with
000058| | Bot,_ -> (*[2]*)Bot
000060| | Top,_ -> (*[35]*)Top
000061| | _,Top -> (*[6]*)Top
000062| | Const c, Const c' -> (*[12]*)Const (c ^ c')
000063|
000064| (* empty : elem -> bool *)
000066|
000067| (* nonempty : elem -> bool *)
000068| let nonempty s = (*[6]*)s <> Bot
000069|
000070|
000071| (** {3 Pretty printing routine } *)
000072|
000073| (* to_string : elem -> unit *)
000074| let to_string s = match s with
000075| | Bot -> "Bot"
000076| | Const c -> "Const \"" ^ c ^ "\""
000077| | Top -> "Top"
000078|
000079| (* pprint : elem -> unit *)
000080| let pprint s = match s with
000081| | Bot -> Format.printf "Bot"
000082| | Const c -> Format.printf "Const \"%s\"" c
000083| | Top -> Format.printf "Top"