LustreTypeChecker (kind2dev@731decdf5fb1.LustreTypeChecker)

module LA = LustreAst

type error_kind =

| Unknown of string
| Impossible of string
| UnboundIdentifier of HString.t
| UnboundModeReference of HString.t
| UnboundNodeName of HString.t
| NotAFieldOfRecord of HString.t
| AssumptionOnCurrentOutput of HString.t
| NoValueForRecordField of HString.t
| IlltypedFieldProjection of TypeCheckerContext.tc_type
| TupleIndexOutOfBounds of int * TypeCheckerContext.tc_type
| IlltypedTupleProjection of TypeCheckerContext.tc_type
| NonConcreteTupleProjection of TypeCheckerContext.LA.expr
| UnequalIteBranchTypes of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedBooleanExpression of TypeCheckerContext.tc_type
| ExpectedIntegerExpression of TypeCheckerContext.tc_type
| Unsupported of string
| UnequalArrayExpressionType
| TypeMismatchOfRecordLabel of HString.t * TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| IlltypedUpdateWithLabel of TypeCheckerContext.tc_type
| IlltypedUpdateWithIndex of TypeCheckerContext.tc_type
| IlltypedUpdate of TypeCheckerContext.tc_type
| ExpectedLabel of TypeCheckerContext.LA.expr
| ExpectedIntegerLiteral of TypeCheckerContext.LA.expr
| IlltypedArraySlice of TypeCheckerContext.tc_type
| ExpectedIntegerTypeForSlice
| IlltypedIndexAccess of TypeCheckerContext.tc_type
| IlltypedMapIndex of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedIntegerTypeForArrayIndex of TypeCheckerContext.tc_type
| IlltypedArrayConcat of bool * TypeCheckerContext.tc_type * TypeCheckerContext.tc_type option
| IlltypedArrow of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| IlltypedFby of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| IlltypedCall of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| IlltypedRecord of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedFunctionType of TypeCheckerContext.tc_type
| IlltypedIdentifier of HString.t * TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| UnificationFailed of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedType of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| EmptyArrayExpression
| ExpectedArrayType of TypeCheckerContext.tc_type
| MismatchedNodeType of HString.t * TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| IlltypedBitNot of TypeCheckerContext.tc_type
| IlltypedUnaryMinus of TypeCheckerContext.tc_type
| ExpectedIntegerTypes of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedNumberOrSetTypes of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedMachineIntegerTypes of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedUnsignedMachineIntegerTypes of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| ExpectedMachineIntegerType of TypeCheckerContext.tc_type
| ExpectedBitShiftConstantOfSameWidth of TypeCheckerContext.tc_type
| ExpectedBitShiftMachineIntegerType of TypeCheckerContext.tc_type
| InvalidConversion of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| NodeArgumentOnLHS of HString.t
| MismatchOfEquationType of TypeCheckerContext.LA.struct_item list option * TypeCheckerContext.tc_type
| DisallowedReassignment of TypeCheckerContext.ty_set
| AssumptionMustBeInputOrOutput of HString.t
| Redeclaration of HString.t
| ExpectedConstant of string * string
| UndeclaredType of HString.t
| EmptySubrange of int * int
| SubrangeArgumentMustBeConstantInteger of TypeCheckerContext.LA.expr
| IntervalMustHaveBound
| ExpectedRecordType of TypeCheckerContext.tc_type
| UnsupportedQuantifiedVariable of HString.t
| InvalidPolymorphicCall of HString.t
| InvalidExtractUpperBound of int * int
| InvalidExtractLowerBound of int * int
| UnsupportedMapType of TypeCheckerContext.tc_type
| ExpectedMapSetType of TypeCheckerContext.tc_type
| CallRequiresExplicitAnnotation of HString.t
| TempOperatorInFuncInterface of NodeId.t
| TempOperatorInFuncTypeAscription
| RefinementTypeArgInConstant of HString.t
| NoIndexAccessInArrayLength of TypeCheckerContext.tc_type
| NestedTypeTemporal of LustreAst.lustre_type
| NestedTypeNodeCall of LustreAst.lustre_type
| UnboundConstructor of HString.t
| ConstructorArityMismatch of HString.t * int * int
| MatchScrutineeNotADT of TypeCheckerContext.tc_type
| UnequalMatchArmTypes of TypeCheckerContext.tc_type * TypeCheckerContext.tc_type
| DuplicateConstructor of HString.t * HString.t * HString.t
| DuplicateConstructorInType of HString.t * HString.t
| ConstructorNameClashWithConst of HString.t * HString.t
| NonWellFoundedDatatype of HString.t
| InvalidDecreasesType of TypeCheckerContext.tc_type
| ADTInLexicographicDecreases of TypeCheckerContext.tc_type
| NonRecursiveADTDecreases of TypeCheckerContext.tc_type
| NonInputInADTDecreasesMeasure of HString.t
| UnsupportedRecursiveAdtField of HString.t * HString.t
| NonUniformRecursiveDatatype of HString.t * HString.t
| MutuallyRecursiveDatatypes of HString.t * HString.t
| UnsupportedRefinementInRecursiveAdtField of HString.t * HString.t
| UnsupportedRefinementInRecursiveAdtInstantiation of HString.t
| DuplicateFieldName of HString.t * HString.t * HString.t
| DuplicateFieldNameInCtor of HString.t * HString.t
| NotAFieldOfADT of HString.t

type error = [

| `LustreTypeCheckerError of Lib.position * error_kind
| `LustreAstInlineConstantsError of Lib.position * LustreAstInlineConstants.error_kind

]

type warning_kind =

| UnusedBoundVariableWarning of HString.t

type warning = [

| `LustreTypeCheckerWarning of Lib.position * warning_kind

]

val warning_message : warning_kind -> string

val error_if_lus_strict : warning_kind -> bool

val error_message : error_kind -> string

val type_error : Lib.position -> error_kind -> ('a, [> error ]) Stdlib.result

type_error returns an Error of tc_result

val type_check_infer_globals : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.t ->
  (TypeCheckerContext.LA.t * TypeCheckerContext.tc_context * [> warning ] list,
    [> error ])
    Stdlib.result

Typechecks the toplevel globals i.e. constant decls and type decls. It returns a Ok (tc_context) if it succeeds or and Error of String if the typechecker fails

val type_check_infer_nodes_and_contracts : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.t ->
  (TypeCheckerContext.tc_context * TypeCheckerContext.LA.t * [> warning ] list,
    [> error ])
    Stdlib.result

Typechecks and infers type for the nodes and contracts. It returns a Ok (tc_context) if it succeeds or and Error of String if the typechecker fails

val tc_ctx_of_contract : 
  ?ignore_modes:bool ->
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.source ->
  TypeCheckerContext.NI.t ->
  TypeCheckerContext.LA.contract ->
  (TypeCheckerContext.LA.contract
   * TypeCheckerContext.tc_context
   * [> warning ] list,
    [> error ])
    Stdlib.result

val extract_exports : 
  TypeCheckerContext.NI.t ->
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.contract ->
  (TypeCheckerContext.tc_context * [> warning ] list, [> error ]) Stdlib.result

val add_ty_params_node_ctx : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t ->
  HString.t list ->
  TypeCheckerContext.tc_context

val add_io_node_ctx : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t ->
  HString.t list ->
  TypeCheckerContext.LA.const_clocked_typed_decl list ->
  TypeCheckerContext.LA.clocked_typed_decl list ->
  TypeCheckerContext.tc_context

val add_local_node_ctx : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.node_local_decl list ->
  TypeCheckerContext.tc_context

val add_full_node_ctx : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t ->
  HString.t list ->
  TypeCheckerContext.LA.const_clocked_typed_decl list ->
  TypeCheckerContext.LA.clocked_typed_decl list ->
  TypeCheckerContext.LA.node_local_decl list ->
  TypeCheckerContext.tc_context

val instantiate_type_variables : 
  TypeCheckerContext.tc_context ->
  Lib.position ->
  TypeCheckerContext.NI.t ->
  TypeCheckerContext.tc_type ->
  TypeCheckerContext.tc_type list ->
  (TypeCheckerContext.tc_type, [> error ]) Stdlib.result

val instantiate_type_variables_expr : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t ->
  TypeCheckerContext.tc_type list ->
  TypeCheckerContext.LA.expr ->
  (TypeCheckerContext.LA.expr, [> error ]) Stdlib.result

val build_node_fun_ty : 
  Lib.position ->
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t ->
  HString.t list ->
  TypeCheckerContext.LA.const_clocked_typed_decl list ->
  TypeCheckerContext.LA.clocked_typed_decl list ->
  (TypeCheckerContext.tc_type
   * TypeCheckerContext.LA.const_clocked_typed_decl list
   * TypeCheckerContext.LA.clocked_typed_decl list
   * [> warning ] list,
    [> error ])
    Stdlib.result

val expand_type_syn_reftype : 
  ?expand_history:bool ->
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.tc_type ->
  (TypeCheckerContext.tc_type, [> error ]) Stdlib.result

val expand_type_syn_reftype_history : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.tc_type ->
  (TypeCheckerContext.tc_type, [> error ]) Stdlib.result

val infer_type_expr : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t option ->
  TypeCheckerContext.LA.expr ->
  (TypeCheckerContext.tc_type * TypeCheckerContext.LA.expr * [> warning ] list,
    [> error ])
    Stdlib.result

Infer type of Lustre expression given a typing context

val bind_pattern_ty : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.tc_type ->
  TypeCheckerContext.LA.pattern ->
  (TypeCheckerContext.tc_context * TypeCheckerContext.LA.pattern, [> error ])
    Stdlib.result

Resolve a match pattern against the type it matches, returning the context the arm's body is checked in and the pattern with each nullary-constructor variable pattern resolved to a constructor pattern

val desugar_generic_index : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t option ->
  TypeCheckerContext.LA.expr ->
  TypeCheckerContext.LA.label_or_index ->
  (TypeCheckerContext.LA.label_or_index, [> error ]) Stdlib.result

Convert the GenericIndex to one of the other indices based on type information

val eq_lustre_type : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.lustre_type ->
  TypeCheckerContext.LA.lustre_type ->
  (bool, [> error ]) Stdlib.result

Check if two lustre types are equal

val tc_ctx_of_contract_node_decl : 
  Lib.position ->
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.contract_node_decl ->
  (TypeCheckerContext.LA.contract_node_decl
   * TypeCheckerContext.tc_context
   * [> warning ] list,
    [> error ])
    Stdlib.result

val tc_ctx_of_node_decl : 
  Lib.position ->
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.LA.node_decl ->
  bool ->
  (TypeCheckerContext.LA.node_decl
   * TypeCheckerContext.tc_context
   * [> warning ] list,
    [> error ])
    Stdlib.result

val expr_contains_set_binop : 
  TypeCheckerContext.tc_context ->
  TypeCheckerContext.NI.t option ->
  TypeCheckerContext.LA.expr ->
  bool

`expr_contains_set_binop e` returns true iff `e` contains set equality, set union or set intersection