Module LustreSyntaxChecks

Check various syntactic properties that do not depend on type information

module LA = LustreAst
type error_kind =
  1. | Unknown of string
  2. | UndefinedLocal of HString.t
  3. | DuplicateLocal of HString.t * Lib.position
  4. | DuplicateOutput of HString.t * Lib.position
  5. | UndefinedOutput of HString.t
  6. | DuplicateProperty of HString.t
  7. | InvalidPropertyName of HString.t
  8. | UndefinedNode of HString.t
  9. | UndefinedContract of HString.t
  10. | DanglingIdentifier of HString.t
  11. | QuantifiedVariableInPre of HString.t
  12. | QuantifiedVariableInNodeArgument of HString.t * HString.t
  13. | SymbolicArrayIndexInNodeArgument of HString.t * HString.t
  14. | QuantifiedVariableInLazyGuardedNodeCall of HString.t * HString.t
  15. | SymbolicArrayIndexInLazyGuardedNodeCall of HString.t * HString.t
  16. | QuantifiedVariableInTypeAscription of HString.t
  17. | SymbolicArrayIndexInTypeAscription of HString.t
  18. | IllegalNodeCall of HString.t * string
  19. | IllegalAnyOp of string
  20. | NodeCallInConstant of HString.t
  21. | NodeCallInGlobalTypeDecl of HString.t
  22. | IllegalTemporalOperator of string * string
  23. | IllegalImportOfStatefulContract of HString.t
  24. | UnsupportedClockedInputOrOutput
  25. | UnsupportedClockedLocal of HString.t
  26. | UnsupportedExpression of LustreAst.expr
  27. | UnsupportedOutsideMerge of LustreAst.expr
  28. | UnsupportedWhen of LustreAst.expr
  29. | UnsupportedParametricDeclaration
  30. | UnsupportedAssignment
  31. | MultAssignArrayDef
  32. | AssumptionVariablesInContractNode
  33. | MisplacedVarInFrameBlock of LustreAst.ident
  34. | MisplacedAssertInFrameBlock
  35. | OpaqueWithoutContract of LustreAst.ident
  36. | TransparentWithoutBody of LustreAst.ident
  37. | IllegalHistoryVar of LustreAst.ident
  38. | InductiveVarsWithArrayConstr of LustreAst.expr
  39. | DuplicatePatternVariable of HString.t
  40. | MissingDecreasesClause of HString.t
  41. | IllegalDecreasesMeasure of HString.t
  42. | MultipleDecreasesClauses of HString.t
  43. | DecreasesClauseInContractNodeDecl of HString.t
  44. | MisplacedDecreasesClause of HString.t
  45. | MisplacedAuto
  46. | LemmaCallOutsideCallStatement of HString.t
  47. | CallStatementCallsNonLemma of HString.t
  48. | InvalidUnderscore
type error = [
  1. | `LustreSyntaxChecksError of Lib.position * error_kind
]
val error_message : error_kind -> string
type warning_kind =
  1. | UnusedBoundVariableWarning of HString.t
type warning = [
  1. | `LustreSyntaxChecksWarning of Lib.position * warning_kind
]
val warning_message : warning_kind -> string
val error_if_lus_strict : warning_kind -> bool
val syntax_check : LA.t -> ([> warning ] list * LA.t, [> error ]) Stdlib.result
val no_quant_vars_in_calls_to_non_inlinable_funcs : TypeCheckerContext.tc_context -> NodeId.Set.t -> LA.t -> ([> warning ] list, [> error ]) Stdlib.result