fth TRIV is
sort Elt
endfth

fmod DEFAULT[Y :: TRIV] is
sort Default[Y] .
subsort Elt.Y < Default[Y] .

op null : -> Default[Y] .
endfmod

fmod RECORD[X :: TRIV] is 
protecting SET[Qid] .
sorts Attribute[X] Attributes[X] Record[X] .
subsorts Attribute[X] < Attributes[X] .

op nil : Attributes[X] .
op (_:_) Qid Elt.X -> Attribute[X] .
op _,_ : [Attributes[X]] [Attributes[X]] -> [Attributes[X]] 
                                                    [assoc comm id: nil] .
op <_> : Attributes[X] -> Record[X] .
op ids : Attributes[X] -> Set[Qid] .

var I : Qid .
var Z : Elt.X .
var ATTS : Attributes[X] .

eq ids(nil) = empty .
eq ids(I : Z) = I .
eq ids(I : Z,ATTS) = I + ids(ATTS) .

cmb (I : Z,ATTS) : Attributes[X] if not(I in ids(ATTS)) .
endfm

fmod BIB-FIELDS is
protecting DEFAULT[MachineInt] .
protecting DEFAULT[List[Qid]] .

sorts Pages Person School Organization Year Month Address ReportType Value .
subsorts MachineInt < Pages .
subsorts School < Organization .

protecting DEFAULT[Year] .
protecting DEFAULT[Month] .
protecting DEFAULT[School] .
protecting DEFAULT[Organization] .
protecting DEFAULT[Address] .
protecting DEFAULT[ReportType] .
protecting DEFAULT[List[Person]]*(__ to _and_) .

subsorts Default[List[Qid]] Default[List[Person]] Default[Pages]
             Default[School] Default[Organization] Default[MachineInt] 
    Default[ReportType] Default[Address] Default[Year] Default[Month] < Value .

op _--_ : MachineInt MachineInt -> [Pages] .

cmb N:MachineInt -- M:MachineInt : Pages if N:MachineInt < M:MachineInt .
eq N:MachineInt -- N:MachineInt = N:MachineInt .
endfm

fmod BIB-ENTRIES is
protecting RECORD[Value] .

sorts Article Book PhDThesis BibEntry .
subsorts Article Book PhDThesis < BibEntry < Record[Value] .

mb < 'author : X:List[Person], 'title : Y:List[Qid], 'journal : Z:List[Qid],
     'year : U:Year, 
      'volume : V:Default[MachineInt], 'number : W:Default[MachineInt],
      'pages : P:Default[Pages], 'month : M:Default[Month], 
      'note : N:Default[List[Qid]] > : Article .

mb < 'author : X:List[Person], 'title : Y:List[Qid], 'journal : Z:List[Qid],
     'year : U:Year, 
      'volume : V:Default[MachineInt], 
      'pages : P:Default[Pages], 'month : M:Default[Month], 
      'note : N:Default[List[Qid]] > : Book .

mb < 'author : X:List[Person], 'title : Y:List[Qid], 'journal : Z:List[Qid],
     'year : U:Year, 
      'number : W:Default[MachineInt],
      'pages : P:Default[Pages], 'month : M:Default[Month], 
      'note : N:Default[List[Qid]] > : Book .

mb < 'editor : X:List[Person], 'title : Y:List[Qid], 'journal : Z:List[Qid],
     'year : U:Year, 
      'volume : V:Default[MachineInt], 
      'pages : P:Default[Pages], 'month : M:Default[Month], 
      'note : N:Default[List[Qid]] > : Book .

mb < 'editor : X:List[Person], 'title : Y:List[Qid], 'journal : Z:List[Qid],
     'year : U:Year, 
      'number : W:Default[MachineInt],
      'pages : P:Default[Pages], 'month : M:Default[Month], 
      'note : N:Default[List[Qid]] > : Book .

mb < 'author : X:Person, 'title : Y:List[Qid], 'school : Z:School,
     'year : U:Year, 
      'type : V:Default[ReportType], 'address : W:Default[Address],
      'month : M:Default[Month], 'note : N:Default[List[Qid]] > : PhDThesis .
endfm