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 usage () =
  31   prerr_endline "Usage: regtest <file.test> ...";
  32   prerr_endline "       regtest (-gen|--gen) <file.cic> ...";
  33   exit 2
  34
  35 let rawsep = "###"
  36 let sep = Pcre.regexp rawsep
  37 let msg_prefix = "*** REGTEST *** "
  38 let print_msg s = prerr_endline (msg_prefix ^ s)
  39
  40 type state = Term | ETerm | EType | EReduced
  41
  42 (* regtest file format
  43  *    < cic term in concrete syntax >
  44  *    separator (* see sep above *)
  45  *    < expected cic term after disambiguation as PPed by CicPp.ppterm >
  46  *    separator (* see sep above *)
  47  *    < expected cic type as per type_of as PPed by CicPp.ppterm >
  48  *    separator (* see sep above *)
  49  *    < expected reduced cic term as PPed by CicPp.ppterm >
  50  *)
  51
  52 type regtest = {
  53   term: string; (* raw cic term *)
  54   eterm: string;  (* expected term *)
  55   etype: string;  (* expected type *)
  56   ereduced: string; (* expected reduced term *)
  57 }
  58
  59   (* this should be the only function here printing on stdout *)
  60 let print_test test fname =
  61   let oc = open_out fname in
  62   output_string oc
  63     (String.concat ""
  64       [ test.term; rawsep ^ "\n";
  65         test.eterm; rawsep ^ "\n";
  66         test.etype; rawsep ^ "\n";
  67         test.ereduced ]);
  68   close_out oc
  69
  70 let parse_regtest =
  71   let term = Buffer.create 1024 in  (* raw term *)
  72   let eterm = Buffer.create 1024 in (* raw expected term *)
  73   let etype = Buffer.create 1024 in (* raw expected type *)
  74   let ereduced = Buffer.create 1024 in (* raw expected reducted term *)
  75   let state = ref Term in
  76   let bump_state () =
  77     match !state with
  78     | Term -> state := ETerm
  79     | ETerm -> state := EType
  80     | EType -> state := EReduced
  81     | EReduced -> assert false
  82   in
  83   let buffer_of_state = function
  84     | Term ->  term | ETerm -> eterm | EType -> etype | EReduced -> ereduced
  85   in
  86   fun fname ->
  87     state := Term;
  88     Buffer.clear term; Buffer.clear eterm; Buffer.clear etype;
  89     Buffer.clear ereduced;
  90     let ic = open_in fname in
  91     (try
  92       while true do
  93         let line = input_line ic in
  94         match line with
  95         | l when Pcre.pmatch ~rex:sep l -> bump_state ()
  96         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
  97       done
  98     with End_of_file -> ());
  99     { term = Buffer.contents term;
 100       eterm = Buffer.contents eterm;
 101       etype = Buffer.contents etype;
 102       ereduced = Buffer.contents ereduced }
 103
 104 let as_expected expected found = (* ignores "term" field *)
 105   let outcome = ref true in
 106   if expected.eterm <> found.eterm then begin
 107     print_msg "Term mismatch";
 108     print_msg "  expected:";
 109     print_msg ("  " ^ expected.eterm);
 110     print_msg "  found:";
 111     print_msg ("  " ^ found.eterm);
 112     outcome := false;
 113   end;
 114   if expected.etype <> found.etype then begin
 115     print_msg "Type mismatch";
 116     print_msg "  expected:";
 117     print_msg ("  " ^ expected.etype);
 118     print_msg "  found:";
 119     print_msg ("  " ^ found.etype);
 120     outcome := false;
 121   end;
 122   if expected.ereduced <> found.ereduced then begin
 123     print_msg "Reduced term mismatch";
 124     print_msg "  expected:";
 125     print_msg ("  " ^ expected.ereduced);
 126     print_msg "  found:";
 127     print_msg ("  " ^ found.ereduced);
 128     outcome := false;
 129   end;
 130   !outcome
 131
 132 let test_this raw_term =
 133   let empty_context = [] in
 134   let (metasenv, cic_term) = BatchParser.parse raw_term in
 135   let cic_type = CicTypeChecker.type_of_aux' metasenv empty_context cic_term in
 136   let cic_reduced = CicReduction.whd empty_context cic_term in
 137   {
 138     term = raw_term;  (* useless *)
 139     eterm = CicPp.ppterm cic_term ^ "\n";
 140     etype = CicPp.ppterm cic_type ^ "\n";
 141     ereduced = CicPp.ppterm cic_reduced ^ "\n";
 142   }
 143
 144 let main () =
 145   if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *)
 146     print_msg "[ Gen mode ]";
 147     for i = 2 to argc - 1 do
 148       let fname = Sys.argv.(i) in
 149       let test_fname = fname ^ ".test" in
 150       print_msg (sprintf "Generating regtest %s -> %s\n ..."
 151         fname test_fname);
 152       let raw_term = (parse_regtest fname).term in
 153       let result = test_this raw_term in
 154       print_test result test_fname
 155     done
 156   end else begin  (* regtest mode *)
 157     prerr_endline "[ Regtest mode ]";
 158     let (ok, nok) = (ref 0, ref []) in
 159     for i = 1 to argc - 1 do
 160       let fname = Sys.argv.(i) in
 161       prerr_endline ("# " ^ fname);
 162       let expected = parse_regtest fname in
 163       let actual = test_this expected.term in
 164       if as_expected expected actual then
 165         incr ok
 166       else
 167         nok := fname :: !nok;
 168     done;
 169     print_msg "Regtest completed:";
 170     print_msg (sprintf "Succeeded: %d" !ok);
 171     print_msg (sprintf "Failed: %d" (List.length !nok));
 172     List.iter (fun fname -> print_msg (sprintf "  %s failed :-(" fname))
 173       (List.rev !nok)
 174   end
 175
 176 let _ = try main () with Invalid_argument _ -> usage ()
 177