Hi list, please find at <http://users.encs.concordia.ca/~vincent/Software_files/download_typecheck.php> a small add-on to HOL-Light which tries to improve slightly the feedback in case of type errors.
This is really a small, fast-written, patch which does not claim for exhaustiveness or elegance of type errors, but I think it already helps a lot more than the originally silent type errors of HOL-Light. In addition, it might of course be buggy. Please give feedback if interested. Also, if you know of something that already does that in a better way, please tell me, I was not able to find any. USAGE Just write the following in your HOL-Light console: # needs "typecheck.ml";; EXAMPLES: As examples, here is a bunch of ill-typed terms along with the exception raised by the native HOL-Light typechecker (basically always the same exception): # `f x /\ f`;; Exception: Failure "typechecking error (initial type assignment)". # `f (x:A) (x:B)`;; Exception: Failure "typechecking error (initial type assignment)". # `1:A`;; Exception: Failure "typechecking error (initial type assignment)". # `T:A`;; Exception: Failure "typechecking error (initial type assignment)". # `APPEND [1] [T]`;; Exception: Failure "typechecking error (initial type assignment)". Now the same ill-typed terms after loading "typecheck.ml": # `f x /\ f`;; Exception: Failure "typechecking error (initial type assignment): f cannot have type _->bool and bool simultaneously". # `f (x:A) (x:B)`;; Exception: Failure "typechecking error (initial type assignment): x cannot have type A and B simultaneously". # `1:A`;; Exception: Failure "typechecking error (initial type assignment): 1 cannot have type num and A simultaneously". # `T:A`;; Exception: Failure "typechecking error (initial type assignment): T cannot have type bool and A simultaneously". # `APPEND [1] [T]`;; Exception: Failure "typechecking error (initial type assignment): T cannot have type bool and num simultaneously". However, some things remain the same: # `1 + &1`;; Exception: Failure "typechecking error (overload resolution)". Best regards, -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_sfd2d_oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
