ternary type checking limitation

[pataei]

Petr4 doesn't support the case where both sub-expressions of e1 ? e2 : e3 have the infinite precision integer type. Code can be found in checker.ml:

type_ternary env ctx cond tru fls : Prog.Expression.t =
  let cond_typed = type_expression env ctx cond in
  let open Expression in 
  assert_bool (tags cond) cond_typed.typ |> ignore;
  let fls_typed = type_expression env ctx fls in
  let tru_typed = type_expression env ctx tru in
  assert_same_type env (tags tru) (tags fls) tru_typed.typ fls_typed.typ |> ignore;
  match tru_typed.typ with
  | Type.Integer ->
     (* TODO this is allowed if cond is compile-time known *)
     failwith "Conditional expressions may not have arbitrary width integer type"
  | t ->
     { expr = Ternary { cond = cond_typed; tru = tru_typed; fls = fls_typed; tags = Info.dummy };
       typ = t;
       dir = Directionless;
       tags = Info.dummy}

However, P4 spec states that: "The first sub-expression e1 must have Boolean type (i.e. “bit” or "bit<1>"), and the second and third sub-expressions must have the same type, which cannot both be infinite-precision integers unless the condition itself can be evaluated at compilation time. This restriction is designed to ensure that the width of the result of the conditional expression can be inferred statically at compile time."

[pataei]

Simple solution: add compile-time-known check to the condition.