607 |
607 |
608 (*brute-force disambiguation via type-inference*) |
608 (*brute-force disambiguation via type-inference*) |
609 val termss = fold_rev (multiply o fst) args [[]]; |
609 val termss = fold_rev (multiply o fst) args [[]]; |
610 val typs = map snd args; |
610 val typs = map snd args; |
611 |
611 |
612 fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy) |
612 fun infer ts = Exn.Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy) |
613 (try (Consts.the_constraint consts)) def_type used freeze (ts ~~ typs) |>> map fst) |
613 (try (Consts.the_constraint consts)) def_type used freeze (ts ~~ typs) |>> map fst) |
614 handle TYPE (msg, _, _) => Exn (ERROR msg); |
614 handle TYPE (msg, _, _) => Exn.Exn (ERROR msg); |
615 |
615 |
616 val err_results = map infer termss; |
616 val err_results = map infer termss; |
617 val errs = map_filter (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results; |
617 val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results; |
618 val results = map_filter get_result err_results; |
618 val results = map_filter Exn.get_result err_results; |
619 |
619 |
620 val ambiguity = length termss; |
620 val ambiguity = length termss; |
621 fun ambig_msg () = |
621 fun ambig_msg () = |
622 if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then |
622 if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then |
623 "Got more than one parse tree.\n\ |
623 "Got more than one parse tree.\n\ |