(* lexicon.sig *)

(* Copyright (C) 2006 Alley Stoughton

   This file is part of crypto, a cryptogram encoder/decoder.  See the
   file COPYING.txt for copying and usage restrictions *)

(* a lexicon based on a linear ordering

   a lexicon represents a set of lists of symbols

   lexicons support efficient matching *)

signature LEXICON =
sig

structure LinOrd : LIN_ORD

type lexicon

(* a lexicon representing the empty set *)

val empty : lexicon

(* add(xs, lex) returns a lexicon that represents the union of {xs} and
   the set represented by lex *)

val add : LinOrd.elem list * lexicon -> lexicon

(* patterns *)

datatype pat = Lit  of LinOrd.elem  (* literal *)
             | Wild of LinOrd.elem  (* wildcard *)

(* a list of pats xs MATCHES a list of symbols ys iff
   length xs = length ys and there is a bijection f from

     { a | Wild a is an element of xs }

   to a set of symbols that is disjoint from

     { a | Lit a is an element of xs }

   such that xs can be turned into ys by:

     replacing each element Lit a by a; and  

     replacing each element Wild a by f a.

   matches(xs, lex) tests whether xs matches at least one list of
   symbols in the set of lists of symbols represented by lex *)

val matches : pat list * lexicon -> bool

end;