Functor TypeInference.Convert

module Convert (T : Nunchaku_core.TermTyped.S) : sig .. end

Parameters:

T : Nunchaku_core.TermTyped.S

type term = T.t

type env

val empty_env : env

Make a new, empty environment. The build function will be used to construct new terms

val convert_ty : env:env ->
       Nunchaku_core.UntypedAST.ty ->
       term TypeInference.or_error

convert ~env ty converts the raw, unscoped type ty into a type from the representation Ty.t. It returns an error if the type is ill-scoped.

val convert_ty_exn : env:env ->
       Nunchaku_core.UntypedAST.ty -> term

Raises ScopingError if the type isnT.t well-scoped

val convert_term : env:env ->
       Nunchaku_core.UntypedAST.term ->
       term TypeInference.or_error

convert ~env ty converts the raw, unscoped type ty into a type from the representation Ty.t. It returns an error if the type is ill-scoped.

val convert_term_exn : env:env ->
       Nunchaku_core.UntypedAST.term -> term

Unsafe version of convert
Raises TypeError if it fails to type properly

val generalize : close:[ `Forall | `Fun | `NoClose ] ->
       term ->
       term *
       term TypeInference.var list

Generalize a T.t t by parametrizing it over its free type variables.
Returns a pair (t', vars) such that, roughly, app t' vars = t, or t' is forall vars t, or t' contains vars

close : decides how t is generalized

`Forall makes t' = forall vars t
`Fun makes t' = fun vars t
`NoClose makes t' = t with meta variables replaced by vars

type statement = (term, term)
       Nunchaku_core.Statement.t

val convert_statement : env:env ->
       Nunchaku_core.UntypedAST.statement ->
       (statement * env)
       TypeInference.or_error

val convert_statement_exn : env:env ->
       Nunchaku_core.UntypedAST.statement ->
       statement * env

Unsafe version of convert

type problem = (term, term)
       Nunchaku_core.Problem.t

val convert_problem : env:env ->
       Nunchaku_core.UntypedAST.statement CCVector.ro_vector ->
       (problem * env)
       TypeInference.or_error

val convert_problem_exn : env:env ->
       Nunchaku_core.UntypedAST.statement CCVector.ro_vector ->
       problem * env