sig
type 'a or_error = [ `Error of string | `Ok of 'a ]
type type_ = TypedSTerm.t
type untyped = STerm.t
type typed = TypedSTerm.t
type loc = ParseLocation.t
exception Error of string
val section : Util.Section.t
module TyBuiltin :
sig
val ty : Builtin.t -> TypeInference.type_ option
val ty_exn : Builtin.t -> TypeInference.type_
end
module Ctx :
sig
type t
val create :
?default:TypeInference.type_ -> unit -> TypeInference.Ctx.t
val copy : TypeInference.Ctx.t -> TypeInference.Ctx.t
val exit_scope : TypeInference.Ctx.t -> unit
val declare :
TypeInference.Ctx.t -> ID.t -> TypeInference.type_ -> unit
val pop_new_types :
TypeInference.Ctx.t -> (ID.t * TypeInference.type_) list
end
val unify :
?loc:TypeInference.loc ->
TypeInference.type_ -> TypeInference.type_ -> unit
val infer_ty_exn :
TypeInference.Ctx.t -> TypeInference.untyped -> TypeInference.type_
val infer_ty :
TypeInference.Ctx.t ->
TypeInference.untyped -> TypeInference.type_ TypeInference.or_error
val infer_exn :
TypeInference.Ctx.t -> TypeInference.untyped -> TypeInference.typed
val infer :
TypeInference.Ctx.t ->
TypeInference.untyped -> TypeInference.typed TypeInference.or_error
val infer_prop_exn :
TypeInference.Ctx.t -> TypeInference.untyped -> TypeInference.typed
val infer_clause_exn :
TypeInference.Ctx.t ->
TypeInference.untyped list -> TypeInference.typed list
val constrain_term_term_exn :
?loc:TypeInference.loc ->
TypeInference.Ctx.t ->
TypeInference.untyped -> TypeInference.untyped -> unit
val constrain_term_type_exn :
?loc:TypeInference.loc ->
TypeInference.Ctx.t ->
TypeInference.untyped -> TypeInference.type_ -> unit
val constrain_term_term :
?loc:TypeInference.loc ->
TypeInference.Ctx.t ->
TypeInference.untyped ->
TypeInference.untyped -> unit TypeInference.or_error
val constrain_term_type :
?loc:TypeInference.loc ->
TypeInference.Ctx.t ->
TypeInference.untyped ->
TypeInference.type_ -> unit TypeInference.or_error
type typed_statement =
(TypeInference.typed, TypeInference.typed, TypeInference.type_,
UntypedAST.attrs)
Statement.t
val infer_statement_exn :
TypeInference.Ctx.t ->
UntypedAST.statement ->
TypeInference.typed_statement * TypeInference.typed_statement list
val infer_statements_exn :
?ctx:TypeInference.Ctx.t ->
UntypedAST.statement Sequence.t ->
TypeInference.typed_statement CCVector.ro_vector
val infer_statements :
?ctx:TypeInference.Ctx.t ->
UntypedAST.statement Sequence.t ->
TypeInference.typed_statement CCVector.ro_vector TypeInference.or_error
end