Structure Preterm

signature Preterm =
sig
  type pretype = Pretype.pretype
  type hol_type = Type.hol_type
  type term = Term.term
  type overinfo = {Name : string,
                   Ty : pretype,
                   Info : Overload.overloaded_op_info,
                   Locn : locn.locn}

  datatype preterm =
    Var of   {Name : string, Ty : pretype, Locn : locn.locn}
  | Const of {Name : string, Thy : string, Ty : pretype, Locn : locn.locn}
  | Overloaded of overinfo
  | Comb of  {Rator: preterm, Rand : preterm, Locn : locn.locn}
  | Abs of   {Bvar : preterm, Body : preterm, Locn : locn.locn}
  | Constrained of {Ptm:preterm, Ty:pretype, Locn:locn.locn}
  | Antiq of {Tm:term, Locn:locn.locn}
  | Pattern of {Ptm:preterm, Locn:locn.locn}
  (* | HackHack of bool -> bool *)
  (* Because of the Locn fields, preterms should *not* be compared
     with the built-in equality, but should use eq defined below.
     To check this has been done everywhere, uncomment this constructor. *)

  val locn : preterm -> locn.locn
  val term_to_preterm : string list -> term -> preterm

  val eq : preterm -> preterm -> bool
  val pdest_eq : preterm -> preterm * preterm
  val lhs : preterm -> preterm
  val head_var : preterm -> preterm
  val ptype_of : preterm -> pretype
  val dest_ptvar : preterm -> (string * pretype * locn.locn)
  val plist_mk_rbinop : preterm -> preterm list -> preterm
  val strip_pcomb : preterm -> preterm * preterm list
  val strip_pforall : preterm -> preterm list * preterm
  val ptfvs : preterm -> preterm list
   (* ptfvs ignores free variables that might be hiding in Pattern, Overload
      or Antiq constructors because these are all of fixed type that can't
      vary; ptfvs is designed to find free variables that might have
      unifiable type variables in their types *)


  (* Performs the first phase of type-checking, altering the types
     attached to the various components of the preterm, but without
     resolving overloading.  The two printing functions are used to
     report errors. *)

  val typecheck_phase1 :
    ((term -> string) * (hol_type -> string)) option -> preterm -> unit

  (* performs overloading resolution, possibly guessing overloads if
     this is both allowed by Globals.guessing_overloads and required by
     ambiguity in the term *)

  val overloading_resolution : preterm -> preterm


  (* converts a preterm into a term.  Will guess type variables for
     unassigned pretypes if Globals.guessing_tyvars is true.
     Will fail if the preterm contains any Overloaded constructors, or
     if the types attached to the leaves aren't valid for the kernel.  *)
  val to_term : preterm -> term


  (* deals with case expressions, which need to be properly typed and
     analysed before they can be converted into type-specific case-
     constants *)
  val remove_case_magic : term -> term

  val post_process_term : (term -> term) ref

  (* essentially the composition of all four of the above *)
  val typecheck:
    ((term -> string) * (hol_type -> string)) option -> preterm -> term

  datatype tcheck_error =
           ConstrainFail of term * hol_type
         | AppFail of term * term
         | OvlNoType of string * hol_type

  val last_tcerror : (tcheck_error * locn.locn) option ref

end;

HOL 4, Kananaskis-10