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 (sprintf "^%s" 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 metasenv after disambiguation (CicMetaSubst.ppmetasenv)  >
  46  *    separator (* see sep above *)
  47  *    < expected cic term after disambiguation (CicPp.ppterm) >
  48  *    separator (* see sep above *)
  49  *    < expected cic type as per type_of (CicPp.ppterm) >
  50  *    separator (* see sep above *)
  51  *    < expected reduced cic term as (CicPp.ppterm) >
  52  *)
  53
  54 type regtest = {
  55   term: string; (* raw cic term *)
  56   emetasenv : string; (* expected metasenv *)
  57   eterm: string;  (* expected term *)
  58   etype: string;  (* expected type *)
  59   ereduced: string; (* expected reduced term *)
  60 }
  61
  62 let print_test test fname =
  63   let oc = open_out fname in
  64   output_string oc
  65     (String.concat ""
  66       [ test.term;
  67         sprintf "%s (* METASENV after disambiguation  *)\n" rawsep;
  68         test.emetasenv;
  69         sprintf "%s (* TERM after disambiguation      *)\n" rawsep;
  70         test.eterm;
  71         sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep;
  72         test.etype;
  73         sprintf "%s (* REDUCED disambiguated term     *)\n" rawsep;
  74         test.ereduced ]);
  75   close_out oc
  76
  77 let parse_regtest =
  78   let term = Buffer.create 1024 in  (* raw term *)
  79   let emetasenv = Buffer.create 1024 in  (* expected metasenv *)
  80   let eterm = Buffer.create 1024 in (* raw expected term *)
  81   let etype = Buffer.create 1024 in (* raw expected type *)
  82   let ereduced = Buffer.create 1024 in (* raw expected reducted term *)
  83   let state = ref Term in
  84   let bump_state () =
  85     match !state with
  86     | Term -> state := EMetasenv
  87     | EMetasenv -> state := ETerm
  88     | ETerm -> state := EType
  89     | EType -> state := EReduced
  90     | EReduced -> assert false
  91   in
  92   let buffer_of_state = function
  93     | Term ->  term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype
  94     | EReduced -> ereduced
  95   in
  96   let clear_buffers () =
  97     List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ]
  98   in
  99   fun fname ->
 100     state := Term;
 101     clear_buffers ();
 102     let ic = open_in fname in
 103     (try
 104       while true do
 105         let line = input_line ic in
 106         match line with
 107         | l when Pcre.pmatch ~rex:sep l -> bump_state ()
 108         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
 109       done
 110     with End_of_file -> ());
 111     { term = Buffer.contents term;
 112       emetasenv = Buffer.contents emetasenv;
 113       eterm = Buffer.contents eterm;
 114       etype = Buffer.contents etype;
 115       ereduced = Buffer.contents ereduced }
 116
 117 let as_expected expected found = (* ignores "term" field *)
 118   let outcome = ref true in
 119   if expected.eterm <> found.eterm then begin
 120     print_msg "Term mismatch";
 121     print_msg "  expected:";
 122     print_msg ("  " ^ expected.eterm);
 123     print_msg "  found:";
 124     print_msg ("  " ^ found.eterm);
 125     outcome := false;
 126   end;
 127   if expected.emetasenv <> found.emetasenv then begin
 128     print_msg "Metasenv mismatch";
 129     print_msg "  expected:";
 130     print_msg ("  " ^ expected.emetasenv);
 131     print_msg "  found:";
 132     print_msg ("  " ^ found.emetasenv);
 133     outcome := false;
 134   end;
 135   if expected.etype <> found.etype then begin
 136     print_msg "Type mismatch";
 137     print_msg "  expected:";
 138     print_msg ("  " ^ expected.etype);
 139     print_msg "  found:";
 140     print_msg ("  " ^ found.etype);
 141     outcome := false;
 142   end;
 143   if expected.ereduced <> found.ereduced then begin
 144     print_msg "Reduced term mismatch";
 145     print_msg "  expected:";
 146     print_msg ("  " ^ expected.ereduced);
 147     print_msg "  found:";
 148     print_msg ("  " ^ found.ereduced);
 149     outcome := false;
 150   end;
 151   !outcome
 152
 153 let test_this raw_term =
 154   let empty_context = [] in
 155   let (metasenv, cic_term) = BatchParser.parse raw_term in
 156   let etype =
 157    try
 158     CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
 159    with
 160     _ -> "MALFORMED"
 161   in
 162   let ereduced =
 163    try
 164     CicPp.ppterm (CicReduction.whd empty_context cic_term)
 165    with
 166     _ -> "MALFORMED"
 167   in
 168   {
 169     term = raw_term;  (* useless *)
 170     emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
 171     eterm = CicPp.ppterm cic_term ^ "\n";
 172     etype = etype ^ "\n";
 173     ereduced = ereduced ^ "\n";
 174   }
 175
 176 let main () =
 177   if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *)
 178     print_msg "[ Gen mode ]";
 179     for i = 2 to argc - 1 do
 180       let fname = Sys.argv.(i) in
 181       let test_fname = fname ^ ".test" in
 182       print_msg (sprintf "Generating regtest %s -> %s\n ..."
 183         fname test_fname);
 184       let raw_term = (parse_regtest fname).term in
 185       let result = test_this raw_term in
 186       print_test result test_fname
 187     done
 188   end else begin  (* regtest mode *)
 189     prerr_endline "[ Regtest mode ]";
 190     let (ok, nok) = (ref 0, ref []) in
 191     for i = 1 to argc - 1 do
 192       let fname = Sys.argv.(i) in
 193       prerr_endline ("# " ^ fname);
 194       try
 195         let expected = parse_regtest fname in
 196         let actual = test_this expected.term in
 197         if as_expected expected actual then
 198           incr ok
 199         else
 200           nok := fname :: !nok;
 201       with e -> nok := fname :: !nok
 202     done;
 203     print_msg "Regtest completed:";
 204     print_msg (sprintf "Succeeded: %d" !ok);
 205     print_msg (sprintf "Failed: %d" (List.length !nok));
 206     List.iter (fun fname -> print_msg (sprintf "  %s failed :-(" fname))
 207       (List.rev !nok)
 208   end
 209
 210 let _ = try main () with Invalid_argument _ -> usage ()
 211