helm/ocaml/cic_notation/test_parser.ml

   1 (* Copyright (C) 2005, 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 _ =
  29   Helm_registry.set "getter.mode" "remote";
  30   Helm_registry.set "getter.url" "http://helm.cs.unibo.it:58081/"
  31
  32   (* ORRIBLE HACK! conversion:
  33    * (Cic.id, string) Hashtbl.t -> (Cic.id, CicNotationtPt.sort_kind) Hashtbl.t
  34    *)
  35 let patch_sort_tbl tbl =
  36   let sort_of_string = function
  37     | "Prop" -> `Prop
  38     | "Set" -> `Set
  39     | "Type" | "?" -> `Type
  40     | "CProp" -> `CProp
  41     | _ -> assert false
  42   in
  43   let tbl' = Hashtbl.create (Hashtbl.length tbl) in
  44   Hashtbl.iter
  45     (fun id sort_str -> Hashtbl.add tbl' id (sort_of_string sort_str))
  46     tbl;
  47   tbl'
  48
  49 let _ =
  50   let module P = CicNotationPt in
  51   let level = ref ~-1 in
  52   let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in
  53   let usage = "test_parser -level { 1 | 2 | 3 }" in
  54   Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage;
  55   if !level = 2 then begin
  56     let id =
  57       CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
  58         (P.Layout (P.Box (P.H,
  59           [
  60             P.Magic
  61               (P.List1
  62                 (P.Layout (P.Box (P.H,
  63                   [ P.Literal (`Symbol "|");
  64                     P.Variable (P.TermVar "ugo");
  65                     P.Magic (P.Opt (P.Layout (P.Box (P.H,
  66                       [ P.Literal (`Symbol ",");
  67                         P.Variable (P.TermVar "pino")]))));
  68                     P.Literal (`Symbol "|");
  69                   ])),
  70                   Some (`Symbol ";")));
  71 (*             P.Literal (`Symbol "+");
  72             P.Magic (P.Opt (P.Layout (P.Box (P.H,
  73               [
  74                 P.Variable (P.TermVar "ugo");
  75                 P.Literal (`Symbol "+");
  76                 P.Variable (P.TermVar "pino")
  77               ])))); *)
  78 (*           P.Variable (P.TermVar "a");
  79             P.Literal (`Symbol "+");
  80             P.Variable (P.TermVar "b"); *)
  81           ])))
  82         (fun env _ ->
  83           prerr_endline "reducing rule" ;
  84           prerr_endline (sprintf "env = [ %s ]" (CicNotationPp.pp_env env));
  85           P.Sort `Prop)
  86     in
  87     CicNotationParser.print_l2_pattern ()
  88   end;
  89   let ic = stdin in
  90   try
  91     printf "Parsing notation level %d\n" !level; flush stdout;
  92     while true do
  93       let line = input_line ic in
  94       let istream = Stream.of_string line in
  95       try
  96         (match !level with
  97         | -1 ->
  98             (match CicNotationParser.parse_phrase istream with
  99             | P.Print t ->
 100                 print_endline (CicNotationPp.pp_term t); flush stdout
 101             | P.Notation (l1, associativity, precedence, l2) ->
 102                 print_endline "Extending notation ..."; flush stdout;
 103                 ignore
 104                   (CicNotationParser.extend l1 ?precedence ?associativity
 105                     (fun env loc ->
 106                       prerr_endline "ENV";
 107                       prerr_endline (CicNotationPp.pp_env env);
 108                       CicNotationFwd.instantiate_level2 env l2))
 109             | P.Interpretation (l2, l3) ->
 110                 print_endline "Adding interpretation ..."; flush stdout;
 111                 let time1 = Unix.gettimeofday () in
 112                 ignore (CicNotationRew.add_interpretation l2 l3);
 113                 let time2 = Unix.gettimeofday () in
 114                 printf "done (patterns compilation took %f seconds)\n"
 115                   (time2 -. time1);
 116                 flush stdout
 117             | P.Render uri ->
 118                 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 119                 let annobj, _, _, id_to_sort, _, _, _ =
 120                   Cic2acic.acic_object_of_cic_object obj
 121                 in
 122                 let annterm =
 123                   match annobj with
 124                   | Cic.AConstant (_, _, _, _, ty, _, _)
 125                   | Cic.AVariable (_, _, _, ty, _, _) -> ty
 126                   | _ -> assert false
 127                 in
 128                 let id_to_sort = patch_sort_tbl id_to_sort in
 129                 let time1 = Unix.gettimeofday () in
 130                 let t, id_to_uri =
 131                   CicNotationRew.ast_of_acic id_to_sort annterm
 132                 in
 133                 let time2 = Unix.gettimeofday () in
 134                 printf "ast creation took %f seconds\n" (time2 -. time1);
 135                 print_endline (CicNotationPp.pp_term t); flush stdout)
 136 (*                 CicNotationParser.print_l2_pattern ()) *)
 137         | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
 138         | 2 ->
 139             let ast = CicNotationParser.parse_ast_pattern istream in
 140             if ast = P.Sort `Prop then
 141               prerr_endline "eureka"
 142             else
 143               prerr_endline ":-("
 144         | 3 -> ignore (CicNotationParser.parse_interpretation istream)
 145         | _ -> Arg.usage arg_spec usage; exit 1);
 146       with CicNotationParser.Parse_error (floc, msg) ->
 147         let (x, y) = P.loc_of_floc floc in
 148         let before = String.sub line 0 x in
 149         let error = String.sub line x (y - x) in
 150         let after = String.sub line y (String.length line - y) in
 151         eprintf "%s\e[01;31m%s\e[00m%s\n" before error after;
 152         prerr_endline (sprintf "at character %d-%d: %s" x y msg)
 153     done
 154   with End_of_file ->
 155     close_in ic
 156