helm/gTopLevel/regtest.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 let argc = Array.length Sys.argv
  29
  30 let rawsep = "###"
  31 let sep = Pcre.regexp (sprintf "^%s" rawsep)
  32 let print s = print_string s
  33 let print_endline s = print_endline s
  34
  35 type state = Term | EMetasenv | ETerm | EType | EReduced
  36
  37 (* regtest file format
  38  *    < cic term in concrete syntax >
  39  *    separator (* see sep above *)
  40  *    < expected metasenv after disambiguation (CicMetaSubst.ppmetasenv)  >
  41  *    separator (* see sep above *)
  42  *    < expected cic term after disambiguation (CicPp.ppterm) >
  43  *    separator (* see sep above *)
  44  *    < expected cic type as per type_of (CicPp.ppterm) >
  45  *    separator (* see sep above *)
  46  *    < expected reduced cic term as (CicPp.ppterm) >
  47  *)
  48
  49 type regtest = {
  50   term: string; (* raw cic term *)
  51   emetasenv : string; (* expected metasenv *)
  52   eterm: string;  (* expected term *)
  53   etype: string;  (* expected type *)
  54   ereduced: string; (* expected reduced term *)
  55 }
  56
  57 let print_test test fname =
  58   let oc = open_out fname in
  59   output_string oc
  60     (String.concat ""
  61       [ test.term;
  62         sprintf "%s (* METASENV after disambiguation  *)\n" rawsep;
  63         test.emetasenv;
  64         sprintf "%s (* TERM after disambiguation      *)\n" rawsep;
  65         test.eterm;
  66         sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep;
  67         test.etype;
  68         sprintf "%s (* REDUCED disambiguated term     *)\n" rawsep;
  69         test.ereduced ]);
  70   close_out oc
  71
  72 let parse_regtest =
  73   let term = Buffer.create 1024 in  (* raw term *)
  74   let emetasenv = Buffer.create 1024 in  (* expected metasenv *)
  75   let eterm = Buffer.create 1024 in (* raw expected term *)
  76   let etype = Buffer.create 1024 in (* raw expected type *)
  77   let ereduced = Buffer.create 1024 in (* raw expected reducted term *)
  78   let state = ref Term in
  79   let bump_state () =
  80     match !state with
  81     | Term -> state := EMetasenv
  82     | EMetasenv -> state := ETerm
  83     | ETerm -> state := EType
  84     | EType -> state := EReduced
  85     | EReduced -> assert false
  86   in
  87   let buffer_of_state = function
  88     | Term ->  term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype
  89     | EReduced -> ereduced
  90   in
  91   let clear_buffers () =
  92     List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ]
  93   in
  94   fun fname ->
  95     state := Term;
  96     clear_buffers ();
  97     let ic = open_in fname in
  98     (try
  99       while true do
 100         let line = input_line ic in
 101         match line with
 102         | l when Pcre.pmatch ~rex:sep l -> bump_state ()
 103         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
 104       done
 105     with End_of_file -> ());
 106     { term = Buffer.contents term;
 107       emetasenv = Buffer.contents emetasenv;
 108       eterm = Buffer.contents eterm;
 109       etype = Buffer.contents etype;
 110       ereduced = Buffer.contents ereduced }
 111
 112 let as_expected expected found = (* ignores "term" field *)
 113   let outcome = ref true in
 114   if expected.eterm <> found.eterm then begin
 115     print_endline "Term mismatch";
 116     print_endline "  expected:";
 117     print_endline ("  " ^ expected.eterm);
 118     print_endline "  found:";
 119     print_endline ("  " ^ found.eterm);
 120     outcome := false;
 121   end;
 122   if expected.emetasenv <> found.emetasenv then begin
 123     print_endline "Metasenv mismatch";
 124     print_endline "  expected:";
 125     print_endline ("  " ^ expected.emetasenv);
 126     print_endline "  found:";
 127     print_endline ("  " ^ found.emetasenv);
 128     outcome := false;
 129   end;
 130   if expected.etype <> found.etype then begin
 131     print_endline "Type mismatch";
 132     print_endline "  expected:";
 133     print_endline ("  " ^ expected.etype);
 134     print_endline "  found:";
 135     print_endline ("  " ^ found.etype);
 136     outcome := false;
 137   end;
 138   if expected.ereduced <> found.ereduced then begin
 139     print_endline "Reduced term mismatch";
 140     print_endline "  expected:";
 141     print_endline ("  " ^ expected.ereduced);
 142     print_endline "  found:";
 143     print_endline ("  " ^ found.ereduced);
 144     outcome := false;
 145   end;
 146   !outcome
 147
 148 let test_this raw_term =
 149   let empty_context = [] in
 150   let (metasenv, cic_term) = BatchParser.parse raw_term in
 151   let etype =
 152    try
 153     CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
 154    with
 155     _ -> "MALFORMED"
 156   in
 157   let ereduced =
 158    try
 159     CicPp.ppterm (CicReduction.whd empty_context cic_term)
 160    with
 161     _ -> "MALFORMED"
 162   in
 163   {
 164     term = raw_term;  (* useless *)
 165     emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
 166     eterm = CicPp.ppterm cic_term ^ "\n";
 167     etype = etype ^ "\n";
 168     ereduced = ereduced ^ "\n";
 169   }
 170
 171 let dump_environment filename =
 172   try
 173     let oc = open_out filename in
 174     CicEnvironment.dump_to_channel oc;
 175     close_out oc
 176   with exc ->
 177     prerr_endline
 178      ("DUMP_ENVIRONMENT FAILURE, uncaught excecption " ^
 179        Printexc.to_string exc) ;
 180     raise exc
 181 ;;
 182
 183 let restore_environment filename =
 184   if Sys.file_exists filename then
 185    begin
 186     try
 187       let ic = open_in filename in
 188       CicEnvironment.restore_from_channel ic;
 189       close_in ic
 190     with exc ->
 191       prerr_endline
 192        ("RESTORE_ENVIRONMENT FAILURE, uncaught excecption " ^
 193          Printexc.to_string exc) ;
 194       raise exc
 195    end
 196   else
 197    CicEnvironment.empty ()
 198 ;;
 199
 200 let main generate dump fnames =
 201  if generate then
 202   begin
 203    (* gen mode *)
 204    print_endline "[ Gen mode ]";
 205    List.iter
 206     (function fname ->
 207       let test_fname = fname ^ ".test" in
 208       let env_fname = fname ^ ".env" in
 209       print_endline (sprintf "Generating regtest %s -> %s\n ..."
 210         fname test_fname);
 211       let raw_term = (parse_regtest fname).term in
 212       let result = test_this raw_term in
 213       print_test result test_fname ;
 214       if dump then dump_environment env_fname ;
 215     ) fnames
 216   end else
 217    begin
 218     (* regtest mode *)
 219     print_endline "[ Regtest mode ]";
 220     let (ok, nok) = (ref 0, ref []) in
 221     List.iter
 222      (function fname ->
 223        let env_fname = fname ^ ".env" in
 224        let test_fname = fname ^ ".test" in
 225        restore_environment env_fname ;
 226        let time = Unix.gettimeofday () in
 227        print ("Processing " ^ fname ^":\t") ;
 228        let is_ok =
 229         try
 230           let expected = parse_regtest test_fname in
 231           let actual = test_this expected.term in
 232           if dump then dump_environment env_fname ;
 233           if as_expected expected actual then
 234            (incr ok ; true)
 235           else
 236            (nok := fname :: !nok ; false)
 237         with e -> (nok := fname :: !nok ; false)
 238        in
 239         let timediff = Unix.gettimeofday () -. time in
 240          print (sprintf "done in %f seconds\t" timediff) ;
 241          print_endline (if is_ok then "\e[01;32m[   OK   ]\e[00m" else "\e[01;31m[ FAILED ]\e[00m")
 242      ) fnames ;
 243     print_endline "*** Summary ***";
 244     print_endline (sprintf "Succeeded: %d" !ok);
 245     print_endline (sprintf "Failed: %d" (List.length !nok));
 246     List.iter (fun fname -> print_endline (sprintf "  %s failed :-(" fname))
 247       (List.rev !nok)
 248   end
 249 ;;
 250
 251 let _ =
 252  let fnames = ref [] in
 253  let gen = ref false in
 254  let dump = ref false in
 255  let nodump = ref false in
 256  let usage = "regtest [OPTION] ... test1 ..." in
 257  let spec =
 258    ["-gen",    Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ;
 259     "--gen",    Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ;
 260     "-dump",   Arg.Set dump, "dumps the final environment" ;
 261     "--dump",   Arg.Set dump, "dumps the final environment" ;
 262     "-nodump", Arg.Set dump, "do not dump the final environment" ;
 263     "--nodump", Arg.Set dump, "do not dump the final environment" ]
 264  in
 265   Arg.parse spec (function filename -> fnames := filename::!fnames ) usage ;
 266   if !fnames = [] then
 267    Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ;
 268   main !gen ((!gen || !dump) && (not !nodump))  !fnames
 269 ;;