(* data.sig *)

(* Copyright (C) 2008 Alley Stoughton

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

(* basic symbol-based data *)

signature DATA =
sig

(* a type sym of symbols, along with linear ordering, lexicon and set
   structures based on this type *)

structure SymLinOrd : LIN_ORD

structure SymLexicon : LEXICON where type LinOrd.elem = SymLinOrd.elem

structure SymSet : SET where type LinOrd.elem = SymLinOrd.elem

type sym = SymLinOrd.elem

(* nil will never be an element of the set of symbol lists represented
   by a sym_lexicon *)

type sym_lexicon = SymLexicon.lexicon

type sym_set = SymSet.set

(* the symbols that may actually be used; so, when we speak of
   the values of type sym, we really mean the elements of the
   sym_set symbols *)

val symbols : sym_set

(* words, lines and messages; words are required to be nonempty *)

type word = sym list

type line = word list

type msg = line list

(* partially decoded symbols, words, lines and messages;
   Old is used to label unchanged symbols, New to label renamed
   symbols; pdw's are required to be nonempty *)

datatype pds = Old of sym | New of sym

type pdw = pds list

type pdl = pdw list

type pdm = pdl list

(* a RENAMING ren is a function from symbols to symbols with the
   property that, for all symbols y, there is a unique symbol x, such
   that ren x = y

   we APPLY a renaming ren to a message by applying ren to each
   symbol of each word of each line of the message

   a DECODING msg' of a message msg RELATIVE TO a set of words xs
   is a message such that:

     each word of msg' is in xs; and

     msg' can be formed by applying some renaming to msg

   a partially decoded message pdm is CONSISTENT WITH a message msg
   iff:

     msg and pdm have the same shape, i.e., they look the same if
     one neglects the identity of the individual sym's and pds's; and

     for all symbols a, either:

       a appears in msg at exactly the same positions that Old a
       appears in pdm; or

       there is a symbol b such that a appears in msg at exactly
       the same positions that New b appears in pdm

   for the following, suppose pdm is a partially decoded message that
   is consistent with the message msg, and that msg' is the unique
   decoding of msg

   we say that pdm is DECODABLE iff if New b appears at some position
   in pdm, then b appears at the same position in msg'

   we say that pdm is DECODED iff pdm is decodable and has no pds's
   with label Old

   If Old a appears in pdm, then the DECODING of a is the letter b
   that appears in msg' at the positions at which Old a appears in pdm
   (i.e., the positions that a appears in msg) *)

end;