(* lexicon-func.sml *)

(* 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 function that takes in a structure LinOrd of signature LIN_ORD and
   returns a structure with signature
   LEXICON where type LinOrd.elem = LinOrd.elem whose LinOrd structure is
   LinOrd *)

functor LexiconFunc(structure LinOrd : LIN_ORD) :>
          LEXICON where type LinOrd.elem = LinOrd.elem =
struct

structure LinOrd = LinOrd

type sym = LinOrd.elem

val compare = LinOrd.compare

(* lexicons are tries

   a lexicon Lexicon(false, [(b1, lex1), (b2, lex2), ..., (bn, lexn)])
   represents the following set of symbol lists:

     {b1 :: bs | bs is in the set represented by lex1} union
     {b2 :: bs | bs is in the set represented by lex2} union
     ...                                               union
     {bn :: bs | bs is in the set represented by lexn}

   a lexicon Lexicon(true, ps) represents the set represented by
   Lexicon(false, ps) union {nil}

   we require that the list ps of a lexicon Lexicon(emp, ps) be sorted in
   ascending order (relative to compare) by its left-hand-sides

   in a lexicon Lexicon(emp, ps @ (b, lex) @ qs), we require that the set
   represented by lex is nonempty *)

datatype lexicon = Lexicon of bool * (sym * lexicon)list

val empty = Lexicon(false, nil)

fun add(nil,     Lexicon(_, ps))   = Lexicon(true, ps)
  | add(c :: cs, Lexicon(emp, ps)) =
      let (* val list : (sym * lexicon)list -> lexicon *)

          fun list nil                    = [(c, add(cs, empty))]
            | list (qs as (b, lex) :: ps) =
                case compare(c, b) of
                     LESS    => (c, add(cs, empty)) :: qs
                   | EQUAL   => (b, add(cs, lex)) :: ps
                   | GREATER => (b, lex) :: list ps
      in Lexicon(emp, list ps) end

datatype pat = Lit  of LinOrd.elem
             | Wild of LinOrd.elem

(* sets of symbols *)

structure Set = SetFunc(structure LinOrd = LinOrd)

(* val symsToAvoid : pat list -> Set.set

    symsToAvoid xs returns { a | Lit a is an element of xs } *)

fun symsToAvoid nil           = Set.fromList nil
  | symsToAvoid (Lit a :: xs) = Set.union(Set.fromList[a], symsToAvoid xs)
  | symsToAvoid (_ :: xs)     = symsToAvoid xs

(* val subst : sym * sym * pat list -> pat list

   subst(a, b, xs) returns the list of patterns that is the same as xs
   except that every occurrence of Wild a in xs has been replaced by Lit b *)

fun subst(a, b, xs) =
      let (* val list : pat list -> pat list *)

          fun list nil            = nil
            | list (Lit c :: xs)  = Lit c :: list xs
            | list (Wild c :: xs) =
                if compare(c, a) = EQUAL
                then Lit b :: list xs
                else Wild c :: list xs
      in list xs end

(* val match : pat list * lexicon * Set.set -> bool

   if avoid is a set of symbols, then a list of pats xs avoid-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 avoid 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.

   if avoid includes all of symsToAvoid xs, then match(xs, lex, avoids)
   tests whether xs avoid-matches at least one list of symbols in the set
   of lists of symbols represented by lex *)

fun match(nil,          Lexicon(emp, _), _)     = emp
  | match(Lit a :: xs,  Lexicon(_, ps),  avoid) =
      let (* val list : (sym * lexicon)list -> bool *)

          fun list nil              = false
            | list ((b, lex) :: ps) =
                case compare(a, b) of
                     LESS    => false
                   | EQUAL   => match(xs, lex, avoid)
                   | GREATER => list ps
      in list ps end
  | match(Wild a :: xs, Lexicon(_, ps),  avoid) =
      let (* val list : (sym * lexicon)list -> bool *)

          fun list nil              = false
            | list ((b, lex) :: ps) =
                if Set.memb(b, avoid)
                then list ps
                else match(subst(a, b, xs),
                           lex,
                           Set.union(Set.fromList[b], avoid)) orelse
                     list ps
      in list ps end

fun matches(xs, lex) = match(xs, lex, symsToAvoid xs)

end;