1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
9 (* verbose error messages on definitions and theorems and parsing. *)
16 let silent= ref false;;
18 let print_mtm m s = if !silent then () else
19 (print_string ("\n"^m^"\n"); print_term s; print_string "\n");;
21 let print_m f m s = if !silent then () else
22 (print_string ("\n"^m^"\n"); f s; print_string "\n";);;
24 let parse_error_msg msg r s = if !silent then failwith msg else (print_string ("Parse error, cannot create "^r^" from \""^s^"\"\n"); failwith msg);;
27 try p s with Failure msg ->
28 print_mtm "Error while processing_1 " s; failwith msg;;
30 let verbose_thm p r s =
31 try p r s with Failure msg ->
32 print_m print_thm "Error while processing_1_thm " s; failwith msg;;
35 try p (s,t) with Failure msg ->
36 print_mtm "Error while processing " s; failwith msg;;
38 let very_verbose_1 p s =
39 print_mtm "VERBOSE MODE (1 argument)" s; p s;;
41 let very_verbose p (s,t) =
42 print_mtm "VERBOSE MODE" s; p (s,t);;
49 let v1 = map dest_var (frees s1) in
50 let v2 = map dest_var (frees s2) in
51 let ss = intersect (map fst v1) (map fst v2) in
52 let f s = mk_type ("prod", [assoc s v1;assoc s v2]) in
53 map (fun s -> ("clash",mk_var (s,aty),f s)) ss;;
55 let rec find_subterms ptm =
56 let r = term_of_preterm o (retypecheck[]) in
57 let m s p = (s,r p,type_of (r p)) in
59 |Varp (s,ty) -> (try (let _ = r ptm in []) with Failure _ ->
60 failwith ("variable typing error: "^s))
61 | Constp (s,pty) -> (try let _ = r ptm in []
62 with Failure _ -> failwith ("constant typing error: "^s))
63 | Combp (s,t) -> (try let _ = r ptm in [] with Failure _ ->
64 if (can r s) && (can r t) then ([m "function head" s; m "function arg" t] @ conflicts (r s) (r t))
65 else if (can r s) then find_subterms t else find_subterms s)
66 | Absp (s,t) -> (try let _ = r ptm in [] with Failure _ ->
67 if (can r s) && (can r t) then [m "absvar" s; m "absbody" t]
68 else if (can r s) then find_subterms t else find_subterms s)
69 | Typing (s,_) -> (try let _ = r ptm in [] with Failure _ ->
70 if (can r s) then [m "user type constraint on term" s] else find_subterms s);;
72 exception Term_of_preterm_error of (string * term * hol_type) list;;
74 let parse_fail ptm = let flag = !type_invention_warning in
75 let r = (type_invention_warning := false; find_subterms ptm) in
76 let _ = type_invention_warning := flag in
77 raise (Term_of_preterm_error r);;
82 let parse_type_verbose s =
83 let (pty,l) = try ((parse_pretype_verbose o lex o explode) s) with
84 Failure msg -> parse_error_msg msg "pretype" s in
85 if l = [] then try (type_of_pretype pty) with
86 Failure msg -> parse_error_msg msg "type" s
87 else failwith ("Unparsed input "^(string_of_lexcodel l)^" following type in string "^s);;
89 let parse_term_verbose s =
90 let lexstream = try lex ( explode s) with
91 Failure msg -> parse_error_msg msg "lex stream" s in
92 let ptm,l = try (parse_preterm_verbose lexstream) with
93 | Failure msg -> parse_error_msg msg "preterm " s
94 | Noparse -> parse_error_msg "preterm" " preterm " (string_of_lexcodel (lex (explode s))) in
96 try (term_of_preterm o (retypecheck [])) ptm
97 with Failure msg -> (report msg; report ("bad input: "^s); parse_fail ptm)
98 else failwith ("Trailing junk "^(string_of_lexcodel l)^" following preterm in string "^s);;
100 let quotexpander_verbose s =
101 if String.sub s 0 1 = ":" then
102 "Debug.parse_type_verbose \""^
103 (String.escaped (String.sub s 1 (String.length s - 1)))^"\""
104 else "Debug.parse_term_verbose \""^(String.escaped s)^"\"";;
109 let set_verbose_parsing() =
110 Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander_verbose));;
112 let restore_parsing() =
113 Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));;