development/thales/chaff/general/template_def.ml

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Author: Thomas C. Hales                                                    *)
   5 (* Date: Feb 7, 2010                                                          *)
   6 (* ========================================================================== *)
   7
   8
   9 (*
  10 Outputs to a file
  11 a formatted HOL Light identifier, as a module with signature.
  12 The author and date information are added as comments.
  13
  14 The file pathname is derived from the root directory, which can be set by the user,
  15 the lowercase of chapter string must match a subdirectory name precisely,
  16 and the identifier is used to create the file name.
  17 *)
  18
  19
  20 module type Template_hol_type = sig
  21
  22   type data =
  23       {
  24         identifier : string;
  25         chapter : string;
  26         author: string;
  27         date:string;
  28         code:string;
  29         comments:string list;
  30         needlist:string list;
  31       }
  32
  33   val output_template_def : data -> unit
  34
  35   val output_template_lemma : data -> unit
  36
  37   val set_root_dir : string-> unit  (* default is "/tmp" *)
  38
  39 end;;
  40
  41 (*
  42 Example:  The following code creates a template identifier file
  43    "/tmp/Trigonometry/azim_def.hl",
  44 populated with the code from def1
  45 *)
  46
  47 (*
  48
  49 open Template_hol;;
  50 let example1() =
  51   let def1 =
  52     {identifier="azim";
  53      chapter="Trigonometry";
  54      author="Thomas C. Hales";
  55      date="Feb 7, 2010";
  56      code="<Insert HOL-Light code for theorem here>";
  57      comments=["This is just a test!"];
  58      needlist=["Multivariate/flyspeck.ml"];
  59     } in
  60  let _ = set_root_dir "/tmp" in
  61    output_template_def def1;;
  62 example1();;
  63
  64 *)
  65
  66 module Template_hol : Template_hol_type =
  67 struct
  68
  69   type data =
  70       {
  71         identifier : string;
  72         chapter : string;
  73         author: string;
  74         date:string;
  75         code:string;
  76         comments: string list;
  77         needlist:string list;
  78       };;
  79
  80   (* Comments and Line Formatting *)
  81
  82   let sep= "/";;
  83   let pad='=';;
  84   let space=' ';;
  85   let emptystring="";;
  86
  87   let unsplit d f = function
  88     | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
  89     | [] -> "";;
  90
  91   let join_lines  = unsplit "\n" (fun x-> x);;
  92   let width = 80 - 6;;
  93
  94   let c_enclose s = "(* "^s^String.make (width - String.length s) space^" *)";;
  95   let pad_line = (String.make width pad);;
  96   let space_line = String.make width space;;
  97
  98   type opt = Def | Lemma;;
  99   let label t = if t=Def then "Definition" else "Lemma";;
 100   let ext t = if t=Def then "_def" else "";;
 101
 102   (* Content *)
 103
 104   let header t dat =
 105     let p = Printf.sprintf in
 106       unsplit "\n" c_enclose [
 107         pad_line;
 108         p"FLYSPECK - BOOK FORMALIZATION";
 109         space_line;
 110         p"%s: %s" (label t) dat.identifier;
 111         p"Chapter: %s" dat.chapter;
 112         p"Author: %s" dat.author;
 113         p"Date: %s" dat.date;
 114         pad_line;
 115       ];;
 116
 117   let more_comments dat =
 118    if (dat.comments =[]) then emptystring else
 119    "(*\n"^(join_lines dat.comments)^"\n*)\n\n\n";;
 120
 121   let neededfiles dat =
 122        if (dat.needlist =[]) then emptystring else
 123       (unsplit "\n" (fun s -> "flyspeck_needs \""^s^"\";;") dat.needlist)^"\n\n\n";;
 124
 125   let body dat =
 126     let p = Printf.sprintf in
 127     let uc = String.capitalize (String.lowercase dat.identifier) in (* HOL Light parsing: cap first char only *)
 128       join_lines [
 129         p"module type %s_def_type = sig" uc;
 130         p"  val %s : thm" dat.identifier;
 131         "end;;\n\n";
 132         neededfiles dat;
 133         p"module %s : %s_def_type = struct\n" uc uc;
 134         p" let %s = " dat.identifier;
 135         dat.code;
 136         "\nend;;\n";
 137       ];;
 138
 139   (* Output *)
 140
 141   let rootdir =ref "/tmp";;
 142   let set_root_dir s = (rootdir := s);;
 143
 144   let filename  t dat = (!rootdir)^sep^(String.lowercase dat.chapter)^sep^dat.identifier^(ext t)^".hl";;
 145
 146   let save_stringarray filename xs =
 147     let oc = open_out filename in
 148       for i=0 to List.length xs -1
 149       do
 150         Pervasives.output_string oc (List.nth xs i ^ "\n");
 151       done;
 152       close_out oc;;
 153
 154   let output_template t dat = save_stringarray (filename t dat)
 155       [header t dat;"\n\n\n";more_comments dat;
 156        body dat];;
 157
 158   let output_template_def dat = output_template Def dat;;
 159   let output_template_lemma dat = output_template Lemma dat;;
 160
 161 end;;
 162
 163