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