ADT StringExprCaml [  ]
/*  StringExprCaml : String -> ExprCaml */

INITIALS

CONSTRUCTORS

SELECTORS
StringExprCaml_nil_String   :                                  -> ExprCaml
StringExprCaml_cons_String   : Expr * Expr                     -> ExprCaml
StringExprCaml_head_String   : ExprCaml                        -> ExprCaml
StringExprCaml_tail_String   : ExprCaml                        -> ExprCaml
StringExprCaml_length_String   : ExprCaml                      -> ExprCaml
StringExprCaml_concat_String   : ExprCaml * ExprCaml           -> ExprCaml
StringExprCaml_isEmptyList_String   : ExprCaml                 -> ExprCaml
StringExprCaml_EQ_String   : ExprCaml * ExprCaml               -> ExprCaml

auxGroundString_ExprCaml: Expr(i)*String->ExprCaml
String_String:->String
subFirstCamlAux:ExprCaml->ExprCaml
predLengthCamlAux:ExprCaml->ExprCaml

isEmptyS_String:->String
isString_nil_String: String->BOOL
isString_cons_String: String->BOOL
isString_head_String: String->BOOL
isString_tail_String: String->BOOL
isString_length_String: String->BOOL
isString_concat_String: String->BOOL
isString_isEmptyList_String: String->BOOL
isString_EQ_String: String->BOOL

AXIOMS

String_String="String"
isEmptyS_String="isEmpty"
subFirstCamlAux(s)=funApp(
                     funApp(valPathEC(concat_String(String_String,".sub")),s),
                       constantEC(intCC("1")))
predLengthCamlAux(s)=NATExprCaml_PRED(StringExprCaml_length_String(s))

auxGroundString_ExprCaml(errorExpr,sub)=
  infixEC(constantEC(stringCC(sub)),"^",Expr_ExprCaml(errorExpr))
auxGroundString_ExprCaml(varExpr(S1),sub)=
  infixEC(constantEC(stringCC(sub)),"^",Expr_ExprCaml(varExpr(S1)))
auxGroundString_ExprCaml(genExpr(nom,arg),sub)=
  if isString_nil_String(nom) then
    constantEC(stringCC(sub))
  else
    if isString_cons_String(nom) then
      if isGenTermCharExpr(head_LExpr(arg)) then
        auxGroundString_ExprCaml(head_LExpr(tail_LExpr(arg)),concat_String(sub,cons_String(genTermCharExpr(head_LExpr(arg)),nil_String)))
      else
        infixEC(constantEC(stringCC(sub)),"^",
          infixEC(funApp(funApp(valPathEC(concat_String(String_String,".make")),constantEC(intCC("1"))),Expr_ExprCaml(head_LExpr(arg))),"^",Expr_ExprCaml(head_LExpr(tail_LExpr(arg))))
        )
      fi
    else
      infixEC(constantEC(stringCC(sub)),"^",Expr_ExprCaml(genExpr(nom,arg)))
    fi
  fi
auxGroundString_ExprCaml(selExpr(S1,L2),sub)=
  infixEC(constantEC(stringCC(sub)),"^",Expr_ExprCaml(selExpr(S1,L2)))
auxGroundString_ExprCaml(eqExpr(E1,E2),sub)=
  infixEC(constantEC(stringCC(sub)),"^",Expr_ExprCaml(eqExpr(E1,E2)))
auxGroundString_ExprCaml(ifExpr(E1,E2,E3),sub)=
  infixEC(constantEC(stringCC(sub)),"^",Expr_ExprCaml(ifExpr(E1,E2,E3)))


StringExprCaml_nil_String=constantEC(stringCC(nil_String))
StringExprCaml_cons_String(C1,S2)=
  if isGenTermCharExpr(C1) then
    auxGroundString_ExprCaml(S2,cons_String(genTermCharExpr(C1),nil_String))
  else 
    infixEC(funApp(funApp(valPathEC(concat_String(String_String,".make")),constantEC(intCC("1"))),Expr_ExprCaml(C1)),"^",Expr_ExprCaml(S2))
  fi
/* This constructor can be better, if C1 and S2 are constants */
StringExprCaml_head_String(E1)=funApp(funApp(valPathEC(concat_String(String_String,".get")),E1),constantEC(intCC("0")))
StringExprCaml_tail_String(E1)=
  funApp(subFirstCamlAux(E1),predLengthCamlAux(E1))
StringExprCaml_length_String(E1)=funApp(valPathEC(concat_String(String_String,".length")),E1)
StringExprCaml_concat_String(E1,E2)=infixEC(E1,"^",E2)
StringExprCaml_isEmptyList_String(E1)=infixEC(E1,"=",constantEC(stringCC("")))
StringExprCaml_EQ_String(E1,E2)=infixEC(E1,"=",E2)


isString_nil_String(s)=EQ_String(s,concat_String("nil_",String_String))
isString_cons_String(s)=EQ_String(s,concat_String("cons_",String_String))
isString_head_String(s)=EQ_String(s,concat_String("head_",String_String))
isString_tail_String(s)=EQ_String(s,concat_String("tail_",String_String))
isString_length_String(s)=EQ_String(s,concat_String("length_",String_String))
isString_concat_String(s)=EQ_String(s,concat_String("concat_",String_String))
isString_isEmptyList_String(s)=EQ_String(s,concat_String(isEmptyS_String,concat_String("List_",String_String)))
isString_EQ_String(s)=EQ_String(s,concat_String("EQ_",String_String))