development/thales/chaff/general/flyspeck_utility.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: leg                                                               *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-10                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 General utilities.
  11
  12 *)
  13
  14
  15
  16 module type Flyspeck_utility_type = sig
  17
  18 (* looks up all constants first defined in a given file.
  19     The file should be specified in the same way as the "flyspeck_needs" statement
  20     Also, the first argument is filetable() from build.hl
  21 *)
  22
  23 val constants_by_file : (string * int) list -> string -> (string * hol_type) list
  24
  25 (* inverse lookup *)
  26
  27 val file_of_constant : (string * int) list -> string -> string
  28
  29
  30 end;;
  31
  32
  33 module Flyspeck_utility  :Flyspeck_utility_type = struct
  34
  35
  36
  37 (* track constants by file *)
  38   let rec findpos c a  = function
  39       [] -> failwith "find"
  40     | b::bs -> if Pervasives.compare a b = 0 then c else findpos (c+1) a bs;;
  41
  42 let rec sublist t a b = match t with
  43    [] -> []
  44   | t0::ts -> if (a>0) then sublist ts (a-1) (b-1) else if (b<=0) then [] else t0::sublist ts 0 (b-1);;
  45
  46 let range_by_table c (m:(string*int)list) (s:string) =
  47   try(
  48     let r = assoc s m in
  49     let i = findpos 0 (s,r) m in
  50     let start = if (i<=0) then 0 else (let (_,j) = List.nth m (i-1) in j) in
  51       sublist c start r)
  52   with Failure "find" -> [];;
  53
  54 let rec rev_assoc_sorted t i = match t with
  55    [] -> failwith "find"
  56   | (x,j)::ts -> if (i>=j) then rev_assoc_sorted ts i else x;;
  57
  58
  59 let constants_by_file   = fun (ftable:(string*int)list) s -> range_by_table (List.rev (constants())) ftable s;;
  60
  61 (* Example: constants_by_file "trigonometry/trig1.hl" *)
  62
  63 let file_of_constant ftable s =
  64    let cs = map fst (List.rev (constants())) in
  65    try (let i = findpos 0 s cs in rev_assoc_sorted (List.rev ftable) i)
  66    with Failure "find" -> "Constant not located";;
  67
  68 (* Example: file_of_constant ftable "packing" *)
  69
  70 end;;