`webdsl-actions.stx`

pdmosses/webdsl-statix/webdslstatix/trans/static-semantics/webdsl-actions.stx
module 

imports
  static-semantics/actions/binops
  static-semantics/actions/built-ins
  static-semantics/actions/emails
  static-semantics/actions/functions

  static-semantics/entities/annotations

  static-semantics/types/built-ins

  static-semantics/webdsl-entities
  static-semantics/webdsl-types
  static-semantics/webdsl

rules // definitions

  defOk(s, GlobalInit(Block(stmts))) :- {}
    new s_init, s_init -DEF-> s,
    stmtsOk(s_init, stmts, VOID()).

rules // unimplemented

  stmtOk(_, _, CaseStmt(_, _), _) :- try { false } | warning $[This statement is not yet implemented].
  stmtOk(_, _, TypeCaseStmt(_, _, _), _) :- try { false } | warning $[This statement is not yet implemented].
  stmtOk(_, _, ThrowStatement(_), _) :- try { false } | warning $[This statement is not yet implemented].
  stmtOk(_, _, TryStatement(_, _), _) :- try { false } | warning $[This statement is not yet implemented].
  stmtOk(_, _, PrefetchForStmt(_, _, _, _), _) :- try { false } | warning $[This statement is not yet implemented].

  typeOfExp(_, exp@FunctionExp(_, _, _)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].
  typeOfExp(_, exp@FunctionRef(_, _, _)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].
  typeOfExp(_, exp@FunctionRefCall(_, _, _, _)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].
  typeOfExp(_, exp@FunctionRefCallPartial(_, _, _, _)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].
  typeOfExp(_, exp@MapCreation(_)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].
  typeOfExp(_, exp@RenderEmailFunctionCall(_)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].
  typeOfExp(_, exp@EmailFunctionCall(_)) = UNTYPED() :- try { false } | warning $[Typing of expression [exp] is not yet implemented].


rules // variable declaration and assignment

  stmtOk(s, _, Stat(exp), _) :-
    expOk(s, exp).

  stmtOk(s, _, Block2Statement(Block(stmts)), rt) :- {  }
    new s_new, s_new -P-> s,
    stmtsOk(s_new, stmts, rt).

  stmtOk(s, s_decl, VarDecl(, ), _) :- {  }
    t == typeOfSort(s, sort),
    inequalType(t, UNTYPED()) | error $[Unknown type [sort]] @sort,
    declareVar(s_decl, x, t),
    @x.type := t.

  stmtOk(, s_decl, VarDeclInit(, , ), _) :- {   }
    t == typeOfSort(s, sort),
    expType == typeOfExp(s, exp),
    typeCompatible(expType, t) | error $[Expression [exp] is not of type [sort], got type [expType]] @exp,
    declareVar(s_decl, x, t),
    @x.type := t.

  stmtOk(s, s_decl, VarDeclInitInferred(, ), _) :- {  }
    t == typeOfExp(s, exp),
    inequalType(t, UNTYPED()) | error $[Unable to infer type of [exp]] @exp,
    declareVar(s_decl, x, t),
    @x.type := t.

  defOk(, GlobalVarDecl(, sort)) :- {  }
    t == typeOfSort(s, sort),
    declareVar(s, x, t),
    declareAnnotation(s, x, DERIVED()).

  defOk(, GlobalVarDeclInit(, , )) :- {   }
    t == typeOfSort(s, sort),
    expType == typeOfExp(s, exp),
    typeCompatible(expType, t) | error $[Expression [exp] is not of type [sort], got type [expType]] @exp,
    declareVar(s, x, t),
    declareAnnotation(s, x, DERIVED()).

  defOk(, GlobalVarDeclInitInferred(, )) :- {  }
    t == typeOfExp(s, exp),
    inequalType(t, UNTYPED()) | error $[Cannot resolve type of expression [exp]],
    declareVar(s, x, t),
    declareAnnotation(s, x, DERIVED()).

   : scope * string
  noDuplicateVarDefs(s, x) :-
    query var filter P*
              and { x' :- x' == (x, _) }
              in s |-> [_].

   : scope * string
  noDuplicateVarDefsInSuper(_, "this"). // allow "this" var to be redefined in sub
  noDuplicateVarDefsInSuper(_, "super"). // allow "super" var to be redefined in sub
  noDuplicateVarDefsInSuper(s_sub, x) :- {   }
    resolveProperty(s_sub, x) == xs,
    withoutAnnotation(xs, OVERRIDABLE()) == nonOverridable,
    amountNonOverridableOk(nonOverridable).

   : list((path * (string * TYPE)))
  amountNonOverridableOk(_) :- false.
  amountNonOverridableOk([]).
  amountNonOverridableOk([_]).

  stmtOk(s, _, Assignment(_, exp), _) :- false | error $[Can only assign to fields or vars (except global or session vars)]. // correct error message for tests
  stmtOk(, _, Assignment(v@Var(), ), _) :- {   }
    variableType(s, x) == t,
    isMutableOrRef(s, x, t),
    expType == typeOfExp(s, exp),
    typeCompatible(expType, t) | error $[Expression [exp] is not of type [t], got type [expType]],
    @v.type := t.

   : scope * string * TYPE
  isMutableOrRef(s, , t) :-
    or(
      isMutableB(s, x),
      isRef(t)
    ) | error $[Variable [x] is not mutable] @x.

   : TYPE -> BOOL
  isRef(REF(_)) = TRUE().
  isRef(_) = FALSE().

  stmtOk(, _, Assignment(FieldAccess(v@FAVar(var), ), ), _) :- {    }
    varType == variableType(s, var),
    @v.type := varType,
    t == typeOfProperty(s, varType, x),
    @x.type := t,
    isMutableProperty(varType, x),
    expType == typeOfExp(s, exp),
    typeCompatible(expType, t) | error $[Expression [exp] is not of type [t], got type [expType]].

  stmtOk(, _, Assignment(FieldAccess(FAExp(lhexp), ), ), _) :- {    }
    lhExpType == typeOfExp(s, lhexp),
    t == typeOfProperty(s, lhExpType, x),
    @x.type := t,
    isMutableProperty(lhExpType, x),
    rhExpType == typeOfExp(s, rhexp),
    typeCompatible(rhExpType, t) | error $[Expression [rhexp] is incompatible with type in left-hand side [t], got type [rhExpType]]. // correct error message for tests

  stmtOk(, _, Assignment(ci@CollectionIndex(_, _), ), _) :-
    typeCompatible(typeOfExp(s, exp), typeOfExp(s, ci)) | error $[Expression [exp] is incompatible with type in left-hand side]. // correct error message for tests

  stmtOk(, _, Assignment(c@Cast(_, _), exp), _) :-
    typeCompatible(typeOfExp(s, exp), typeOfExp(s, c)).

rules // if statements and expressions

  stmtOk(, _, If(, Block(then), Block(else)), ) :- { }
    equalType(typeOfExp(s, c), bool(s)) | error $[Condition should be of type bool] @c,
    new s_then, s_then -P-> s,
    stmtsOk(s_then, then, rt),
    new s_else, s_else -P-> s,
    stmtsOk(s_else, else, rt).

  typeOfExp(, IfExp(ce, ie, ee)) =  :- { }
    ct == typeOfExp(s, ce),
    equalType(ct, bool(s)) | error $[Condition should be of type bool, [ct] given],
    it == typeOfExp(s, ie),
    et == typeOfExp(s, ee),
    typeCompatible(et, it) | error $[Type of else-expression ([et]) should be compatible with type of if-expression ([it])].

rules // loops

  stmtOk(, _, ForStmt(, srt, , OptFilterSome(f), Block(stmts)), rt) :- {  }
    typeOfSort == typeOfSort(s, srt),
    typeOfExp == typeOfExp(s, exp),
    or(
      equalTypeB(LIST(typeOfSort), typeOfExp),
      equalTypeB(SET(typeOfSort), typeOfExp)
    ) | error $[Must be a list or set of type [typeOfSort], [typeOfExp] given] @exp,
    new s_for, s_for -P-> s,
    forLoopFilterOk(s_for, f),
    forLoopStmtsOk(s_for, x, typeOfSort, stmts, rt),
    @x.type := typeOfSort.

  stmtOk(, _, ForStmtInferred(, exp, OptFilterSome(f), Block(stmts)), rt) :- {  }
    typeOfExp == typeOfExp(s, exp),
    t == stripGenericType(typeOfExp),
    new s_for, s_for -P-> s,
    forLoopFilterOk(s_for, f),
    forLoopStmtsOk(s_for, x, t, stmts, rt),
    @x.type := t.

  stmtOk(, _, ForAllStmt(, srt, OptFilterSome(f), Block(stmts)), rt) :- { }
    typeOfSort == typeOfSort(s, srt),
    new s_for, s_for -P-> s,
    forLoopFilterOk(s_for, f),
    forLoopStmtsOk(s_for, x, typeOfSort, stmts, rt),
    @x.type := typeOfSort.

  stmtOk(, _, ForCountStmt(, fromExp, toExp, Block(stmts)), rt) :- { }
    intType == int(s),
    equalType(typeOfExp(s, fromExp), intType) | error $[From expression should have type Int],
    equalType(typeOfExp(s, toExp)  , intType) | error $[To expression should have type Int],
    new s_for, s_for -P-> s,
    forLoopStmtsOk(s_for, x, intType, stmts, rt),
    @x.type := intType.

   : scope * string * TYPE * list(Statement) * TYPE
  forLoopStmtsOk(, , t, stmts, rt) :-
    declareVar(s_for, x, t),
    declareAnnotation(s_for, x, DERIVED()), // abuse derived annotation to declare immutability of x
    stmtsOk(s_for, stmts, rt).

   : scope * Filter
  forLoopFilterOk(s, f). // TO-DO

  stmtOk(, _, WhileStmt(, Block(stmts)), rt) :- {}
    equalType(typeOfExp(s, exp), bool(s)) | error $[Condition should be of type bool] @exp,
    new s_while, s_while -P-> s,
    stmtsOk(s_while, stmts, rt).

rules // return statements

  stmtOk(s, _, r@Return(), ) :- {}
    inequalType(returnType, UNTYPED()) | error $[Return statement not allowed here] @r,
    inequalType(returnType, VOID()) | error $[No return type specified in this context] @exp,
    returnExpType == typeOfExp(s, exp),
    typeCompatible(returnExpType, returnType) | error $[Must return an expression of type [returnType], [returnExpType] given] @exp.

  stmtOk(s, _, @ReturnEmpty(), ) :-
    inequalType(returnType, UNTYPED()) | error $[Return statement not allowed here] @r,
    equalType(returnType, VOID()) | error $[Must return an expression of type [returnType]] @r.

rules // variable references

  typeOfExp(s, Var()) =  :-
    variableType(s, x) == t,
    @x.type := t.

  typeOfSimpleExp(s, SimpleVar()) =  :-
    variableType(s, x) == t,
    @x.type := t.

  typeOfExp(s, FieldAccess(FAGlobal(), _)) = UNTYPED() :- try { false } | warning $[Typing of global field access not yet implemented].
  typeOfExp(s, FieldAccess(FASession(), _)) = UNTYPED() :- try { false } | warning $[Typing of global field access not yet implemented].

  typeOfExp(, FieldAccess(FAVar(), )) =  :- {}
    variableType(s, var) == varType,
    @var.type := varType,
    typeOfProperty(s, varType, x) == propertyType,
    @x.type := propertyType.

  typeOfExp(, FieldAccess(FAExp(exp), )) =  :- {}
    typeOfExp(s, exp) == t,
    typeOfProperty(s, t, x) == propertyType,
    @x.type := propertyType.

  typeOfSimpleExp(, SimpleFieldAccess(exp, )) =  :- {}
    typeOfSimpleExp(s, exp) == t,
    typeOfProperty(s, t, x) == propertyType,
    @x.type := propertyType.

  typeOfPlaceholderExp(, PHFieldAccess(exp, )) =  :- {}
    typeOfExp(s, exp) == t,
    typeOfProperty(s, t, x) == propertyType,
    @x.type := propertyType.

   : scope * TYPE * string -> TYPE
  typeOfProperty(_, t, _) = UNTYPED() :- false | error $[Field access is only allowed on native classes and entities, [t] given].
  typeOfProperty(s, REF(t), x) = typeOfProperty(s, t, x).
  typeOfProperty(_, ENTITY(_, s), x) = t :-
    propertyType(s, x) == t.
  typeOfProperty(_, NATIVECLASS(_, s), x) = t :-
    propertyType(s, x) == t.

rules // lists and sets

  typeOfExp(s, ListCreation([])) = UNTYPED() :- false | error $[Type cannot be determined for empty untyped list creation].
  typeOfExp(, lc@ListCreation([hd | ])) = LIST() :-
    t == typeOfExp(s, hd), // first element of the untyped list creation determines the type
    typesCompatibleWith(typesOfExps(s, tl), t) | error $[Not all elements are compatible with type [t]] @tl,
    @lc.type := LIST(t).

  typeOfExp(, tlc@TypedListCreation(sort, )) = LIST() :-
    typeOfSort(s, sort) == t,
    typesCompatibleWith(typesOfExps(s, exps), t) | error $[Not all elements are compatible with type [t]] @exps,
    @tlc.type := LIST(t).

  typeOfExp(s, SetCreation([])) = UNTYPED() :- false | error $[Type cannot be determined for empty untyped set creation].
  typeOfExp(, sc@SetCreation([hd | ])) = SET() :-
    t == typeOfExp(s, hd), // first element of the untyped set creation determines the type
    typesCompatibleWith(typesOfExps(s, tl), t) | error $[Not all elements are compatible with type [t]] @tl,
    @sc.type := SET(t).

  typeOfExp(, tsc@TypedSetCreation(sort, )) = SET() :-
    typeOfSort(s, sort) == t,
    typesCompatibleWith(typesOfExps(s, exps), t) | error $[Not all elements are compatible with type [t]] @exps,
    @tsc.type := SET(t).

  typeOfExp(s, ci@CollectionIndex(c, x)) =  :-
    t == typeOfCollectionIndex(s, c, x),
    @ci.type := t.

  typeOfPlaceholderExp(s, ci@PHCollectionIndex(c, x)) =  :-
    t == typeOfCollectionIndex(s, c, x),
    @ci.type := t.

   : scope * Exp * Exp -> TYPE
  typeOfCollectionIndex(, c, x) = t :- { }
    ct == typeOfExp(s, c),
    xt == typeOfExp(s, x),
    indexedAccessAllowed(ct),
    typeCompatible(xt, int(s)) | error $[Index must be of type Int, [xt] given], // correct error message for tests
    t == stripGenericType(ct).

   : TYPE
  indexedAccessAllowed(_).
  indexedAccessAllowed(SET(_)) :- false | error $[Indexed access \[\] is only allowed for List<type> and Set<type>].

  typeOfExp(s, ForExp2Exp(forExp)) = typeOfForExp(s, forExp).

  typeOfExp(, OrForExp(forExp)) =  :-
    bool == bool(s),
    typeOfForExp(s, forExp) == LIST(bool).

  typeOfExp(, AndForExp(forExp)) =  :-
    bool == bool(s),
    typeOfForExp(s, forExp) == LIST(bool).

rules // list comprehension

   : scope * ForExp -> TYPE
  typeOfForExp(, ForExpInferred(e1, , e2, _, _)) = LIST(t) :- {    }
    new s_e1, s_e1 -P-> s,
    collectionType == typeOfExp(s, e2),
    varType == stripGenericType(collectionType),
    declareVar(s_e1, x, varType),
    t == typeOfExp(s_e1, e1),
    @x.type := varType.
    // TO-DO: implement filter and group by typechecking

  typeOfForExp(, ForExp(e1, x, , , _, _)) = LIST(t) :- {    }
    new s_e1, s_e1 -P-> s,
    collectionType == typeOfExp(s, e2),
    varType == stripGenericType(collectionType),
    stripGenericType(collectionType) == typeOfSort(s, sort) | error $["type of [e2] is not a collection of type [sort]"],
    declareVar(s_e1, x, varType),
    t == typeOfExp(s_e1, e1).
    // TO-DO: implement filter and group by typechecking

rules // test

  defOk(s, Test(_, Block(stmts))) :- {}
    new s_test, s_test -F-> s,
    stmtsOk(s_test, stmts, UNTYPED()).

rules // misc

  stmtOk(s, _, ValidateStatement(validateExp, messageExp), _) :- validateOk(s, validateExp, messageExp).
  stmtOk(s, _, NamedValidateStatement(_, validateExp, messageExp), _) :- validateOk(s, validateExp, messageExp).