1signature Preterm =
2sig
3  type pretype = Pretype.pretype
4  type hol_type = Type.hol_type
5  type term = Term.term
6
7  datatype tcheck_error = datatype typecheck_error.tcheck_error
8  type error = typecheck_error.error
9  val mkExn : error -> exn
10
11  datatype preterm = datatype Preterm_dtype.preterm
12
13  type 'a in_env = 'a Pretype.in_env
14  type 'a errM = (Pretype.Env.t,'a,error) errormonad.t
15  type 'a seqM = (Pretype.Env.t,'a) seqmonad.seqmonad
16  val smash : ('s,'a,error) errormonad.t -> 's -> 'a
17
18  val locn : preterm -> locn.locn
19  val term_to_preterm : string list -> term -> preterm in_env
20
21  val eq : preterm -> preterm -> bool
22  val pdest_eq : preterm -> preterm * preterm
23  val lhs : preterm -> preterm
24  val head_var : preterm -> preterm
25  val ptype_of : preterm -> pretype in_env
26  val dest_ptvar : preterm -> (string * pretype * locn.locn)
27  val plist_mk_rbinop : preterm -> preterm list -> preterm
28  val strip_pcomb : preterm -> preterm * preterm list
29  val strip_pforall : preterm -> preterm list * preterm
30  val ptfvs : preterm -> preterm list
31   (* ptfvs ignores free variables that might be hiding in Pattern, Overload
32      or Antiq constructors because these are all of fixed type that can't
33      vary; ptfvs is designed to find free variables that might have
34      unifiable type variables in their types *)
35
36
37  (* Performs the first phase of type-checking, altering the types
38     attached to the various components of the preterm, but without
39     resolving overloading.  The two printing functions are used to
40     report errors. *)
41
42  val typecheck_phase1 :
43    ((term -> string) * (hol_type -> string)) option -> preterm -> unit errM
44
45  (* performs overloading resolution, possibly guessing overloads if
46     this is both allowed by Globals.guessing_overloads and required by
47     ambiguity in the term *)
48
49  val overloading_resolution : preterm -> (preterm * bool) errM
50  val overloading_resolutionS : preterm -> preterm seqM
51  val report_ovl_ambiguity : bool -> unit errM
52
53
54  (* converts a preterm into a term.  Will guess type variables for
55     unassigned pretypes if Globals.guessing_tyvars is true.
56     Will fail if the preterm contains any Overloaded constructors, or
57     if the types attached to the leaves aren't valid for the kernel.  *)
58  val to_term : preterm -> term in_env
59
60
61  (* deals with case expressions, which need to be properly typed and
62     analysed before they can be converted into type-specific case-
63     constants *)
64  val remove_case_magic : term -> term
65
66  val post_process_term : (term -> term) ref
67
68  (* essentially the composition of all four of the above *)
69  val typecheck:
70    ((term -> string) * (hol_type -> string)) option -> preterm -> term errM
71  val typecheckS : preterm -> term seqM
72
73  val last_tcerror : (tcheck_error * locn.locn) option ref
74
75end
76