ADT PatternCaml [  ]

INITIALS
valueNamePC : String                           -> PatternCaml /* var */
anyPC       :                                  -> PatternCaml /* _ */
constantPC  : ConstantCaml                     -> PatternCaml /* 1 */
productPC   : LPatternCaml                     -> PatternCaml /* 2,3,9 */
consListPC  : LPatternCaml                     -> PatternCaml /* [2;4;5] */
labelPC     : LLabelPatternCaml                -> PatternCaml /* t=6 */

CONSTRUCTORS
asPC        : PatternCaml * String             -> PatternCaml /* 5 as v */
orPC        : PatternCaml * PatternCaml        -> PatternCaml /* 4 | 3 */
constructorPC: String * PatternCaml            -> PatternCaml /* Cons(3) */
typePC      : PatternCaml * TypeExprCaml       -> PatternCaml /* 4:int */

SELECTORS
StringOfPatternCaml:PatternCaml(i)->String
isProductPC:PatternCaml(i)->BOOL
EQ_PatternCaml(c): PatternCaml(i) * PatternCaml(i)  -> BOOL

AXIOMS

isProductPC(valueNamePC(s))=FALSE
isProductPC(anyPC)=FALSE
isProductPC(constantPC(con))=FALSE
isProductPC(productPC(lp))=TRUE
isProductPC(consListPC(lp))=FALSE
isProductPC(labelPC(lp))=FALSE
isProductPC(asPC(p,s))=FALSE
isProductPC(orPC(p1,p2))=FALSE
isProductPC(constructorPC(s,p))=FALSE
isProductPC(typePC(p,t))=FALSE

StringOfPatternCaml(valueNamePC(S))=S
StringOfPatternCaml(anyPC)="_"
StringOfPatternCaml(constantPC(C1))=StringOfConstantCaml(C1)
StringOfPatternCaml(productPC(L1))=StringOfLPatternCaml(L1,",")
StringOfPatternCaml(consListPC(L1))=
  concat_String("[",
  concat_String(StringOfLPatternCaml(L1,";"),"]"))
StringOfPatternCaml(labelPC(L1))=StringOfLLabelPatternCaml(L1)
StringOfPatternCaml(asPC(P1,S2))=
  concat_String("(",
  concat_String(StringOfPatternCaml(P1),
  concat_String(") as ",S2)))
StringOfPatternCaml(orPC(P1,P2))=
  concat_String("(",
  concat_String(StringOfPatternCaml(P1),
  concat_String(") | (",
  concat_String(StringOfPatternCaml(P2),")"))))	
StringOfPatternCaml(constructorPC(S1,P2))=
  if isProductPC(P2) then 
    if isEmptyList_LPatternCaml(LPatternCamlOfProductPC(P2)) then
      S1
    else
      concat_String(S1,
      concat_String("(",
      concat_String(StringOfPatternCaml(P2),")")))
    fi
  else
    concat_String(S1,
    concat_String("(",
    concat_String(StringOfPatternCaml(P2),")")))
  fi
StringOfPatternCaml(typePC(P1,T2))=
  concat_String("(",
  concat_String(StringOfPatternCaml(P1),
  concat_String(") : (",
  concat_String(StringOfTypeExprCaml(T2),")"))))	


EQ_PatternCaml(X,Y) = FALSE