
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"