text_formalization/general/debug.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: General                                                      *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-13                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* verbose error messages on definitions and theorems and parsing. *)
  10
  11
  12 module Debug = struct
  13
  14   open Parser_verbose;;
  15
  16   let silent= ref false;;
  17
  18   let print_mtm m s = if !silent then () else
  19    (print_string ("\n"^m^"\n"); print_term s; print_string "\n");;
  20
  21  let print_m f m s = if !silent then () else
  22    (print_string ("\n"^m^"\n"); f s; print_string "\n";);;
  23
  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);;
  25
  26   let verbose_1 p s =
  27     try p s with Failure msg ->
  28     print_mtm "Error while processing_1 " s; failwith msg;;
  29
  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;;
  33
  34   let verbose p (s,t) =
  35     try p (s,t) with Failure msg ->
  36      print_mtm "Error while processing " s; failwith msg;;
  37
  38   let very_verbose_1 p s =
  39     print_mtm "VERBOSE MODE (1 argument)" s; p s;;
  40
  41   let very_verbose p (s,t) =
  42     print_mtm "VERBOSE MODE" s;  p (s,t);;
  43
  44 (*
  45 Type and Term parsing
  46 *)
  47
  48  let conflicts s1 s2 =
  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;;
  54
  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
  58   match ptm with
  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);;
  71
  72 exception Term_of_preterm_error of (string * term * hol_type) list;;
  73
  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);;
  78
  79
  80
  81
  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);;
  88
  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
  95   if l = [] then
  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);;
  99
 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)^"\"";;
 105
 106
 107 unset_jrh_lexer
 108
 109  let set_verbose_parsing() =
 110    Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander_verbose));;
 111
 112  let restore_parsing() =
 113       Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));;
 114
 115 set_jrh_lexer
 116
 117
 118 end;;