1signature Pretype =
2sig
3
4datatype pretype = datatype Pretype_dtype.pretype
5
6structure Env : sig
7  type t
8  val lookup : t -> int -> pretype option
9  val update : (int * pretype) -> t -> t
10  val empty : t
11  val new : t -> t * int
12  val toList : t -> (int * pretype option) list
13end
14
15type error = typecheck_error.error
16type 'a in_env = (Env.t,'a,error) errormonad.t
17
18val tyvars : pretype -> string list in_env
19val new_uvar : pretype in_env
20val ref_occurs_in : int * pretype -> bool in_env
21val ref_equiv : int * pretype -> bool in_env
22val has_unbound_uvar : pretype -> bool in_env
23val mk_fun_ty : pretype * pretype -> pretype
24
25val unify : pretype -> pretype -> unit in_env
26val can_unify : pretype -> pretype -> bool in_env
27
28val apply_subst : Env.t -> pretype -> pretype
29
30val rename_typevars : string list -> pretype -> pretype in_env
31val rename_tv : string list -> pretype ->
32                (Env.t * (string * pretype) list, pretype, error) errormonad.t
33val fromType : Type.hol_type -> pretype
34val remove_made_links : pretype -> pretype in_env
35val replace_null_links :
36    pretype -> (Env.t * string list, pretype, error) errormonad.t
37val clean : pretype -> Type.hol_type
38val toTypeM : pretype -> Type.hol_type in_env
39val toType : pretype -> Type.hol_type
40val chase : pretype -> pretype in_env
41
42val pp_pretype : pretype -> HOLPP.pretty
43
44val termantiq_constructors : (pretype,Term.term) parse_type.tyconstructors
45val typantiq_constructors : (pretype,Type.hol_type) parse_type.tyconstructors
46
47end
48
49(*
50   [chase pty]  If pty is of the form (dom --> rng), once all necessary
51   uvar references have been followed, returns rng.
52
53   [rename_typvars avds pty]  Avoiding type variables with names from avds,
54   renames Vartypes into uvar references.
55
56   [has_unbound_uvar pty] Returns true if pty includes (after chasing bound
57   uvars), any unbound uvars.
58
59   [mk_fun_ty (dom,rng)] Makes the pretype corresponding to the function space
60   from dom to rng.
61*)
62