jHOLLight/caml/raw_printer.hl

   1 let clear_goalstack() =
   2   current_goalstack := [];;
   3
   4
   5 let top_goalstate() =
   6   if !current_goalstack = [] then
   7     (null_meta, [], fun _ [th] -> th)
   8   else
   9     hd (!current_goalstack);;
  10
  11
  12 let raw_print_string str =
  13   print_string ("$begin$" ^ str ^ "$end$");;
  14
  15
  16 let raw_string_of_int i = string_of_num i;;
  17
  18
  19 let raw_string_of_bool b = if b then "true" else "false";;
  20
  21
  22 let raw_string_of_string str = "\"" ^ str ^ "\"";;
  23
  24
  25 let rec raw_string_of_type =
  26   function
  27       (Tyapp(name, args)) -> "Tyapp(\"" ^ name ^ "\"[" ^ String.concat "," (map raw_string_of_type args) ^ "])"
  28     | (Tyvar v) -> "Tyvar(\"" ^ v ^ "\")";;
  29
  30
  31
  32 let rec raw_string_of_term =
  33   function
  34       Var(name,ty) -> "Var(\"" ^ name ^ "\"," ^ raw_string_of_type ty ^ ")"
  35     | Const(name,ty) -> "Const(\"" ^ name ^ "\"," ^ raw_string_of_type ty ^ ")"
  36     | Comb(f,a) -> "Comb(" ^ raw_string_of_term f ^ "," ^ raw_string_of_term a ^ ")"
  37     | Abs(v,b) -> "Abs(" ^ raw_string_of_term v ^ "," ^ raw_string_of_term b ^ ")";;
  38
  39
  40
  41
  42 let raw_string_of_list el_type el_f list =
  43   let str = String.concat ";" (map el_f list) in
  44     "List(" ^ el_type ^ ",[" ^ str ^ "])";;
  45
  46
  47
  48 let raw_string_of_thm th =
  49   let c = raw_string_of_term (concl th) in
  50   let h = raw_string_of_list "Term" raw_string_of_term (hyp th) in
  51     "Theorem(" ^ h ^ "," ^ c ^ ")";;
  52
  53
  54
  55 let raw_string_of_pair f_fst f_snd p =
  56   "Pair(" ^ f_fst (fst p) ^ "," ^ f_snd (snd p) ^ ")";;
  57
  58
  59
  60 let raw_string_of_goal (g:goal) =
  61   let assumptions = raw_string_of_list "Pair(String,Theorem)" (raw_string_of_pair raw_string_of_string raw_string_of_thm) (fst g) in
  62   let c = raw_string_of_term (snd g) in
  63     "Goal(" ^ assumptions ^ "," ^ c ^ ")";;
  64
  65
  66
  67 let raw_string_of_goalstate (g:goalstate) =
  68   let s (_,b,_) = b in
  69   let goals = raw_string_of_list "Goal" raw_string_of_goal (s g) in
  70     "Goalstate("^goals^")";;