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 | EMetasenv | 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   emetasenv : string; (* expected metasenv *)
  55   eterm: string;  (* expected term *)
  56   etype: string;  (* expected type *)
  57   ereduced: string; (* expected reduced term *)
  58 }
  59
  60   (* this should be the only function here printing on stdout *)
  61 let print_test test fname =
  62   let oc = open_out fname in
  63   output_string oc
  64     (String.concat ""
  65       [ test.term; rawsep ^ "\n";
  66         test.emetasenv; rawsep ^ "\n";
  67         test.eterm; rawsep ^ "\n";
  68         test.etype; rawsep ^ "\n";
  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 | EReduced -> ereduced
  89   in
  90   fun fname ->
  91     state := Term;
  92     Buffer.clear term; Buffer.clear emetasenv; Buffer.clear eterm;
  93     Buffer.clear etype; Buffer.clear ereduced;
  94     let ic = open_in fname in
  95     (try
  96       while true do
  97         let line = input_line ic in
  98         match line with
  99         | l when Pcre.pmatch ~rex:sep l -> bump_state ()
 100         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
 101       done
 102     with End_of_file -> ());
 103     { term = Buffer.contents term;
 104       emetasenv = Buffer.contents emetasenv;
 105       eterm = Buffer.contents eterm;
 106       etype = Buffer.contents etype;
 107       ereduced = Buffer.contents ereduced }
 108
 109 let as_expected expected found = (* ignores "term" field *)
 110   let outcome = ref true in
 111   if expected.eterm <> found.eterm then begin
 112     print_msg "Term mismatch";
 113     print_msg "  expected:";
 114     print_msg ("  " ^ expected.eterm);
 115     print_msg "  found:";
 116     print_msg ("  " ^ found.eterm);
 117     outcome := false;
 118   end;
 119   if expected.etype <> found.etype then begin
 120     print_msg "Type mismatch";
 121     print_msg "  expected:";
 122     print_msg ("  " ^ expected.etype);
 123     print_msg "  found:";
 124     print_msg ("  " ^ found.etype);
 125     outcome := false;
 126   end;
 127   if expected.ereduced <> found.ereduced then begin
 128     print_msg "Reduced term mismatch";
 129     print_msg "  expected:";
 130     print_msg ("  " ^ expected.ereduced);
 131     print_msg "  found:";
 132     print_msg ("  " ^ found.ereduced);
 133     outcome := false;
 134   end;
 135   !outcome
 136
 137 let test_this raw_term =
 138   let empty_context = [] in
 139   let (metasenv, cic_term) = BatchParser.parse raw_term in
 140   let etype =
 141    try
 142     CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
 143    with
 144     _ -> "MALFORMED"
 145   in
 146   let ereduced =
 147    try
 148     CicPp.ppterm (CicReduction.whd empty_context cic_term)
 149    with
 150     _ -> "MALFORMED"
 151   in
 152   {
 153     term = raw_term;  (* useless *)
 154     emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
 155     eterm = CicPp.ppterm cic_term ^ "\n";
 156     etype = etype ^ "\n";
 157     ereduced = ereduced ^ "\n";
 158   }
 159
 160 let main () =
 161   if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *)
 162     print_msg "[ Gen mode ]";
 163     for i = 2 to argc - 1 do
 164       let fname = Sys.argv.(i) in
 165       let test_fname = fname ^ ".test" in
 166       print_msg (sprintf "Generating regtest %s -> %s\n ..."
 167         fname test_fname);
 168       let raw_term = (parse_regtest fname).term in
 169       let result = test_this raw_term in
 170       print_test result test_fname
 171     done
 172   end else begin  (* regtest mode *)
 173     prerr_endline "[ Regtest mode ]";
 174     let (ok, nok) = (ref 0, ref []) in
 175     for i = 1 to argc - 1 do
 176       let fname = Sys.argv.(i) in
 177       prerr_endline ("# " ^ fname);
 178       try
 179         let expected = parse_regtest fname in
 180         let actual = test_this expected.term in
 181         if as_expected expected actual then
 182           incr ok
 183         else
 184           nok := fname :: !nok;
 185       with e -> nok := fname :: !nok
 186     done;
 187     print_msg "Regtest completed:";
 188     print_msg (sprintf "Succeeded: %d" !ok);
 189     print_msg (sprintf "Failed: %d" (List.length !nok));
 190     List.iter (fun fname -> print_msg (sprintf "  %s failed :-(" fname))
 191       (List.rev !nok)
 192   end
 193
 194 let _ = try main () with Invalid_argument _ -> usage ()
 195