Typing (Smirnov.Mardukml

SPDX-License-Identifier: LGPL-3.0-or-later

val initial_context : (string * Ast.mltype) list

val subst_var : int -> Ast.qf_mltype -> Ast.qf_mltype -> Ast.qf_mltype

val instantiate : Ast.mltype -> int -> Ast.qf_mltype * int

val quantify : 
  Ast.mltype ->
  (string * Ast.mltype) list ->
  int ->
  (Ast.qf_mltype * int list) * int

val apply_subst : 
  (int * Ast.qf_mltype) list ->
  Ast.mltype ->
  Ast.qf_mltype * int list

val apply_subst_ctx : 
  (int * Ast.qf_mltype) list ->
  ('a * Ast.mltype) list ->
  ('a * (Ast.qf_mltype * int list)) list

val occurs : int -> Ast.qf_mltype -> bool

val unify : 
  (Ast.qf_mltype * Ast.qf_mltype) list ->
  (int * Ast.qf_mltype) list option

val hm_typechecker : Ast.mlterm -> Ast.mltype