ADT ConstantCaml [  ]

INITIALS
intCC       : String                           -> ConstantCaml
floatCC     : String                           -> ConstantCaml
charCC      : Char                             -> ConstantCaml
stringCC    : String                           -> ConstantCaml
consCC      : String                           -> ConstantCaml

CONSTRUCTORS

SELECTORS
StringOfNAT: NAT(i) -> String
StringOfConstantCaml: ConstantCaml(i)  -> String
changeQuoteString: String(i) -> String
/* String from a character with ASCII code greather than 32 */
StringOfPrintableChar: Char -> String
EQ_ConstantCaml(c): ConstantCaml(i) * ConstantCaml(i)  -> BOOL

AXIOMS

StringOfNAT(X)=
  if EQ_NAT(X,ZERO) then 
    "0"
  else
    if LT(X,9) then 
      cons_String(charOfNAT(ADD(X,48)),nil_String)
    else 
      concat_String(
        StringOfNAT(DIV(X,10)), 
        cons_String(charOfNAT(ADD(MOD(X,10),48)),nil_String))
    fi 
  fi

changeQuoteString(s)=
  if EQ_String(s,"") then 
    nil_String
  else
    if EQ_Char(head_String(s),'\"') then
      concat_String("\\\"",changeQuoteString(tail_String(s)))
    else
      if EQ_Char(head_String(s),'\\') then
        concat_String("\\\\",changeQuoteString(tail_String(s)))
      else
        cons_String(head_String(s),changeQuoteString(tail_String(s)))
      fi
    fi
  fi

StringOfPrintableChar(C1)=
  if EQ_Char(C1,'\'') then
    "\'\\\'\'"
  else
    if EQ_Char(C1,'\\') then
      "\'\\\\\'"
    else
      cons_String('\'',cons_String(C1,cons_String('\'',nil_String)))
    fi
  fi

StringOfConstantCaml(intCC(S1))=S1
StringOfConstantCaml(floatCC(S1))=S1
/* Characters with ASCII code less than 32 shoul be
   printed as \002 */
StringOfConstantCaml(charCC(C1))=
  if LT(asciiOfChar(C1),10) then
    concat_String("\'\\00",
    concat_String(StringOfNAT(asciiOfChar(C1)),"\'"))
  else
    if LT(asciiOfChar(C1),32) then
      concat_String("\'\\0",
      concat_String(StringOfNAT(asciiOfChar(C1)),"\'"))
    else 
      StringOfPrintableChar(C1)
    fi
  fi
StringOfConstantCaml(stringCC(S1))=
  concat_String("\"",concat_String(changeQuoteString(S1),"\""))
StringOfConstantCaml(consCC(S1))=S1

EQ_ConstantCaml(intCC(S1),intCC(S2)) = EQ_String(S1,S2)
EQ_ConstantCaml(intCC(S1),floatCC(S2)) = FALSE
EQ_ConstantCaml(intCC(S1),charCC(C2)) = FALSE
EQ_ConstantCaml(intCC(S1),stringCC(S2)) = FALSE
EQ_ConstantCaml(intCC(S1),consCC(S2)) = FALSE
EQ_ConstantCaml(floatCC(S1),intCC(S2)) = FALSE
EQ_ConstantCaml(floatCC(S1),floatCC(S2)) = EQ_String(S1,S2)
EQ_ConstantCaml(floatCC(S1),charCC(C2)) = FALSE
EQ_ConstantCaml(floatCC(S1),stringCC(S2)) = FALSE
EQ_ConstantCaml(floatCC(S1),consCC(S2)) = FALSE
EQ_ConstantCaml(charCC(C1),intCC(S2)) = FALSE
EQ_ConstantCaml(charCC(C1),floatCC(S2)) = FALSE
EQ_ConstantCaml(charCC(C1),charCC(C2)) = EQ_Char(C1,C2)
EQ_ConstantCaml(charCC(C1),stringCC(S2)) = FALSE
EQ_ConstantCaml(charCC(C1),consCC(S2)) = FALSE
EQ_ConstantCaml(stringCC(S1),intCC(S2)) = FALSE
EQ_ConstantCaml(stringCC(S1),floatCC(S2)) = FALSE
EQ_ConstantCaml(stringCC(S1),charCC(C2)) = FALSE
EQ_ConstantCaml(stringCC(S1),stringCC(S2)) = EQ_String(S1,S2)
EQ_ConstantCaml(stringCC(S1),consCC(S2)) = FALSE
EQ_ConstantCaml(consCC(S1),intCC(S2)) = FALSE
EQ_ConstantCaml(consCC(S1),floatCC(S2)) = FALSE
EQ_ConstantCaml(consCC(S1),charCC(C2)) = FALSE
EQ_ConstantCaml(consCC(S1),stringCC(S2)) = FALSE
EQ_ConstantCaml(consCC(S1),consCC(S2)) = EQ_String(S1,S2)