Expr.mag

declare type PGGExpr;
declare attributes PGGExpr: free_vars;

declare type PGGExpr_FreeVar: PGGExpr;
declare attributes PGGExpr_FreeVar: name;

declare type PGGExpr_Unop: PGGExpr;
declare attributes PGGExpr_Unop: op, arg1, name, prefix, format;

declare type PGGExpr_Binop: PGGExpr;
declare attributes PGGExpr_Binop: op, arg1, arg2, name, infix, format;

declare type PGGExpr_Seqop: PGGExpr;
declare attributes PGGExpr_Seqop: op, args, name, infix;

declare type PGGExpr_Const: PGGExpr;
declare attributes PGGExpr_Const: val;

declare type PGGExpr_All: PGGExpr;
declare attributes PGGExpr_All: args;

declare type PGGExpr_Any: PGGExpr;
declare attributes PGGExpr_Any: args;

intrinsic Print(x :: PGGExpr_FreeVar)
  {Print.}
  printf "%o", x`name;
end intrinsic;

INTRNAME := func<f | Type(f) eq Intrinsic select GetIntrinsicName(f) else "<unknown>">;

intrinsic Print(x :: PGGExpr_Unop)
  {"}
  if assigned x`format then
    printf x`format, x`arg1;
  elif x`prefix then
    printf "(%o %o)", x`name, x`arg1;
  else
    printf "%o(%o)", x`name, x`arg1;
  end if;
end intrinsic;


intrinsic Print(x :: PGGExpr_Binop)
  {"}
  if assigned x`format then
    printf x`format, x`arg1, x`arg2;
  elif x`infix then
    printf "(%o %o %o)", x`arg1, x`name, x`arg2;
  else
    printf "%o(%o, %o)", x`name, x`arg1, x`arg2;
  end if;
end intrinsic;

intrinsic Print(x :: PGGExpr_Seqop)
  {"}
  if x`infix and #x`args ge 1 then
    if #x`args eq 1 then
      Print(x`args[1]);
    else
      printf "(%o)", Join([Sprint(a) : a in x`args], " " cat x`name cat " ");
    end if;
  else
    printf "%o([%o])", x`name, Join([Sprint(a) : a in x`args], ", ");
  end if;
end intrinsic;

intrinsic Print(x :: PGGExpr_Const)
  {"}
  printf "%o", x`val;
end intrinsic;

intrinsic Print(x :: PGGExpr_All)
  {"}
  case #x`args:
  when 0:
    printf "true";
  when 1:
    Print(x`args[1]);
  else
    printf "(%o)", Join([Sprint(y) : y in x`args], " and ");
  end case;
end intrinsic;

intrinsic Print(x :: PGGExpr_Any)
  {"}
  case #x`args:
  when 0:
    printf "false";
  when 1:
    Print(x`args[1]);
  else
    printf "(%o)", Join([Sprint(y) : y in x`args], " or ");
  end case;
end intrinsic;

intrinsic FreeVariables(x :: PGGExpr) -> {}
  {The free variables in the expression.}
  if not assigned x`free_vars then
    x`free_vars := PowerSet(Strings()) ! _FreeVariables(x);
  end if;
  return x`free_vars;
end intrinsic;

intrinsic PGG_Expression_FreeVariable(name :: MonStgElt) -> PGGExpr_FreeVar
  {The free variable with the given name.}
  x := New(PGGExpr_FreeVar);
  x`name := name;
  return x;
end intrinsic;

intrinsic PGG_Expression_UnOp(op, arg1 :: PGGExpr : Prefix:=false, Name:=false, Format:=false) -> PGGExpr_Unop
  {The unary operation op (a function or intrinsic) with argument arg1.}
  x := New(PGGExpr_Unop);
  x`op := op;
  x`arg1 := arg1;
  if Format cmpeq false then
    x`name := Name cmpeq false select INTRNAME(op) else Name;
    x`prefix := Prefix;
  else
    x`format := Format;
  end if;
  return x;
end intrinsic;

intrinsic PGG_Expression_BinOp(op, arg1 :: PGGExpr, arg2 :: PGGExpr : Infix:=false, Name:=false, Format:=false) -> PGGExpr_Binop
  {The binary operation op (a function or intrinsic) with arguments arg1 and arg2.}
  x := New(PGGExpr_Binop);
  x`op := op;
  x`arg1 := arg1;
  x`arg2 := arg2;
  if Format cmpeq false then
    x`infix := Infix;
    x`name := Name cmpeq false select INTRNAME(op) else Name;
  else
    x`format := Format;
  end if;
  return x;
end intrinsic;

intrinsic PGG_Expression_SeqOp(op, args : Infix:=false, Name:=false) -> PGGExpr_Seqop
  {The operation op with one argument, the sequence args.}
  x := New(PGGExpr_Seqop);
  x`op := op;
  x`args := args;
  x`infix := Infix;
  x`name := Name cmpeq false select INTRNAME(op) else Name;
  return x;
end intrinsic;

intrinsic PGG_Expression_Const(val) -> PGGExpr_Const
  {The constant expression val.}
  x := New(PGGExpr_Const);
  x`val := val;
  return x;
end intrinsic;

intrinsic PGG_Expression_All(args) -> PGGExpr_All
  {The expression evaluating to true if all its arguments are true.}
  x := New(PGGExpr_All);
  x`args := args;
  return x;
end intrinsic;

intrinsic PGG_Expression_Any(args) -> PGGExpr_Any
  {The expression evaluating to true if any of its arguments are true.}
  x := New(PGGExpr_Any);
  x`args := args;
  return x;
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_FreeVar) -> {}
  {"}
  return {x`name};
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_Unop) -> {}
  {"}
  return FreeVariables(x`arg1);
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_Binop) -> {}
  {"}
  return FreeVariables(x`arg1) join FreeVariables(x`arg2);
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_Const) -> {}
  {"}
  return {};
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_Seqop) -> {}
  {"}
  return #x`args eq 0 select {} else &join[FreeVariables(arg) : arg in x`args];
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_All) -> {}
  {"}
  return #x`args eq 0 select {} else &join[FreeVariables(arg) : arg in x`args];
end intrinsic;

intrinsic _FreeVariables(x :: PGGExpr_Any) -> {}
  {"}
  return #x`args eq 0 select {} else &join[FreeVariables(arg) : arg in x`args];
end intrinsic;

intrinsic Evaluate(x :: PGGExpr, vars :: UserProgram) -> .
  {Evaluates x.}
  return _Evaluate(x, vars);
end intrinsic;

intrinsic Evaluate(x :: PGGExpr, vars :: Assoc) -> .
  {Evaluates x.}
  return _Evaluate(x, func<n | vars[n]>);
end intrinsic;

intrinsic EvaluateLazy(x :: PGGExpr, lazy_vars :: Assoc : Recursive:=false) -> ., .
  {Evaluates x.}
  store := NewStore();
  if Recursive then
    function vars(name)
      ok, x := StoreIsDefined(store, name);
      if ok then
        return x;
      end if;
      x := lazy_vars[name](vars);
      StoreSet(store, name, x);
      return x;
    end function;
  else
    function vars(name)
      ok, x := StoreIsDefined(store, name);
      if ok then
        return x;
      end if;
      x := lazy_vars[name]();
      StoreSet(store, name, x);
      return x;
    end function;
  end if;
  return _Evaluate(x, vars), vars;
end intrinsic;

intrinsic EvaluateLazy(x :: PGGExpr, lazy_vars :: UserProgram : Recursive:=false) -> ., .
  {Evaluates x.}
  store := NewStore();
  if Recursive then
    function vars(name)
      ok, x := StoreIsDefined(store, name);
      if ok then
        return x;
      end if;
      x := lazy_vars(name, vars);
      StoreSet(store, name, x);
      return x;
    end function;
  else
    function vars(name)
      ok, x := StoreIsDefined(store, name);
      if ok then
        return x;
      end if;
      x := lazy_vars(name);
      StoreSet(store, name, x);
      return x;
    end function;
  end if;
  return _Evaluate(x, vars), vars;
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_FreeVar, vars) -> .
  {Evaluates x.}
  return vars(x`name);
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_Unop, vars) -> .
  {"}
  return x`op(Evaluate(x`arg1, vars));
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_Binop, vars) -> .
  {"}
  return x`op(Evaluate(x`arg1, vars), Evaluate(x`arg2, vars));
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_Const, vars) -> .
  {"}
  return x`val;
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_Seqop, vars) -> .
  {"}
  return x`op([Evaluate(arg, vars) : arg in x`args]);
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_All, vars) -> .
  {"}
  for arg in x`args do
    if not Evaluate(arg, vars) then
      return false;
    end if;
  end for;
  return true;
end intrinsic;

intrinsic _Evaluate(x :: PGGExpr_Any, vars) -> .
  {"}
  for arg in x`args do
    if Evaluate(arg, vars) then
      return true;
    end if;
  end for;
  return false;
end intrinsic;