1structure typecheck_error = 2struct 3 datatype tcheck_error = 4 ConstrainFail of Term.term * Type.hol_type * string 5 | AppFail of Term.term * Term.term * string 6 | OvlNoType of string * Type.hol_type 7 | OvlTooMany 8 | OvlFail 9 | Misc of string 10 11 type error = tcheck_error * locn.locn 12 fun errorMsg tc = 13 case tc of 14 ConstrainFail (_,_,msg) => msg 15 | AppFail (_,_,msg) => msg 16 | OvlNoType(s,_) => 17 ("Couldn't infer type for overloaded name "^s) 18 | OvlFail => "Overloading constraints were unsatisfiable" 19 | OvlTooMany => 20 "There was more than one resolution of overloaded constants" 21 | Misc s => s 22 23 local 24 open Feedback 25 in 26 fun mkExn (tc, loc) = 27 mk_HOL_ERRloc "Preterm" "type-analysis" loc (errorMsg tc) 28 29 end (* local *) 30 31 32end (* struct *) 33