text_formalization/general/hol_pervasives.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* HOL LIGHT pervasives                                                       *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-04-15                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11 This module contains things in HOL Light that clash and get overwriten.
  12 This file needs to be loaded immediately after
  13 tactics.ml and lib.ml to get the intended values.
  14 *)
  15
  16
  17 (* from tactics *)
  18
  19 module Hol_pervasives = struct
  20
  21 let e tac = refine(by(VALID tac));;
  22
  23 let r n = refine(rotate n);;
  24
  25 let g t =
  26   let fvs = sort (<) (map (fst o dest_var) (frees t)) in
  27   (if fvs <> [] then
  28      let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
  29      warn true ("Free variables in goal: "^errmsg)
  30    else ());
  31    set_goal([],t);;
  32
  33 let b() =
  34   let l = !current_goalstack in
  35   if length l = 1 then failwith "Can't back up any more" else
  36   current_goalstack := tl l;
  37   !current_goalstack;;
  38
  39 let p() =
  40   !current_goalstack;;
  41
  42 (* HOL Light lib, in general raises Failure _
  43    unlike Ocaml List, which raises Not_found.  *)
  44
  45 let assoc = assoc;;
  46
  47 let hd = hd;;
  48
  49 let tl = tl;;
  50
  51 let sort = sort;;
  52
  53 let prove = prove;;
  54
  55 let zip = zip;;
  56
  57 let find = find;;
  58
  59 let ISPECL = ISPECL;;
  60
  61
  62 (* abs, sqrt, .... *)
  63
  64 end;;