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