ADT CharExprCaml [  ]
/*  CharExprCaml : Char -> ExprCaml */

INITIALS

CONSTRUCTORS

SELECTORS
CharExprCaml_charOfNAT   : Expr                              -> ExprCaml
CharExprCaml_AsciiOfChar   : ExprCaml                         -> ExprCaml
CharExprCaml_LTChar   : ExprCaml * ExprCaml              -> ExprCaml
CharExprCaml_EQ_Char   : ExprCaml * ExprCaml              -> ExprCaml

auxGroundChar_ExprCaml: Expr(i)*NAT -> ExprCaml
isChar_charOfNAT:String->BOOL
isChar_AsciiOfChar:String->BOOL
isChar_LTChar:String->BOOL
isChar_EQ_Char:String->BOOL

Char_String:->String

/* Decides if the given expression is a Ground Term composed
   only of generators that is a constant character */
isGenTermCharExpr:Expr(i)->BOOL
/* Returns the constant value of the term composed only of
   generators that receive */
genTermCharExpr: Expr(i) -> Char

AXIOMS

auxGroundChar_ExprCaml(errorExpr,cant)=
  funApp(valPathEC(concat_String(Char_String,".chr")),infixEC(constantEC(intCC(StringOfNAT(cant))),"+",Expr_ExprCaml(errorExpr)))
auxGroundChar_ExprCaml(varExpr(S1),cant)=
  funApp(valPathEC(concat_String(Char_String,".chr")),infixEC(constantEC(intCC(StringOfNAT(cant))),"+",Expr_ExprCaml(varExpr(S1))))
auxGroundChar_ExprCaml(genExpr(nom,arg),cant)=
  if isNAT_ZERO(nom) then
    constantEC(charCC(charOfNAT(cant)))
  else
    if isNAT_SUC(nom) then
      auxGroundChar_ExprCaml(head_LExpr(arg),SUC(cant))
    else
      funApp(valPathEC(concat_String(Char_String,".chr")),infixEC(constantEC(intCC(StringOfNAT(cant))),"+",Expr_ExprCaml(genExpr(nom,arg))))
    fi
  fi
auxGroundChar_ExprCaml(selExpr(nom,arg),cant)=funApp(valPathEC(concat_String(Char_String,".chr")),infixEC(constantEC(intCC(StringOfNAT(cant))),"+",Expr_ExprCaml(selExpr(nom,arg))))
auxGroundChar_ExprCaml(eqExpr(E1,E2),cant)=funApp(valPathEC(concat_String(Char_String,".chr")),infixEC(constantEC(intCC(StringOfNAT(cant))),"+",Expr_ExprCaml(eqExpr(E1,E2))))
auxGroundChar_ExprCaml(ifExpr(E1,E2,E3),cant)=funApp(valPathEC(concat_String(Char_String,".chr")),infixEC(constantEC(intCC(StringOfNAT(cant))),"+",Expr_ExprCaml(ifExpr(E1,E2,E3))))

/* This constructor can be better if e is an integer
   constantEC(charCC(charOfNAT(...(e)))) */
CharExprCaml_charOfNAT(e)=auxGroundChar_ExprCaml(e,0)
  /* funApp(valPathEC(concat_String(Char_String,".chr")),Expr_ExprCaml(e)) */
CharExprCaml_AsciiOfChar(e)=funApp(valPathEC("Char.code"),e)
CharExprCaml_LTChar(E1,E2)=infixEC(E1,"<",E2)
CharExprCaml_EQ_Char(E1,E2)=infixEC(E1,"=",E2)

Char_String="Char"
isChar_charOfNAT(s)=EQ_String(s,"charOfNAT")
isChar_AsciiOfChar(s)=EQ_String(s,concat_String("asciiOf",Char_String))
isChar_LTChar(s)=EQ_String(s,"ltChar")
isChar_EQ_Char(s)=EQ_String(s,"EQ_Char")

isGenTermCharExpr(errorExpr)=FALSE
isGenTermCharExpr(varExpr(S1))=FALSE
isGenTermCharExpr(genExpr(nom,arg))=
  if isChar_charOfNAT(nom) then
    isGenTermNATExpr(head_LExpr(arg))
  else
    FALSE
  fi
isGenTermCharExpr(selExpr(S1,L2))=FALSE
isGenTermCharExpr(eqExpr(E1,E2))=FALSE
isGenTermCharExpr(ifExpr(E1,E2,E3))=FALSE

genTermCharExpr(errorExpr)=ERROR
genTermCharExpr(varExpr(S1))=ERROR
genTermCharExpr(genExpr(nom,arg))=charOfNAT(genTermNATExpr(head_LExpr(arg)))
genTermCharExpr(selExpr(S1,L2))=ERROR
genTermCharExpr(eqExpr(E1,E2))=ERROR
genTermCharExpr(ifExpr(E1,E2,E3))=ERROR