helm/ocaml/cic_disambiguation/cicTextualParser2.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 let debug = true
  27 let debug_print s =
  28   if debug then begin
  29     prerr_endline "<NEW_TEXTUAL_PARSER>";
  30     prerr_endline s;
  31     prerr_endline "</NEW_TEXTUAL_PARSER>"
  32   end
  33
  34 open Printf
  35
  36 exception Parse_error of string
  37
  38 let choice_of_uri (uri: string) =
  39   let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in
  40   (uri, (fun _ _ _ -> cic))
  41
  42 let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
  43
  44 let term = Grammar.Entry.create grammar "term"
  45 let term0 = Grammar.Entry.create grammar "term0"
  46 (* let tactic = Grammar.Entry.create grammar "tactic" *)
  47 (* let tactical = Grammar.Entry.create grammar "tactical" *)
  48
  49 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
  50 (* let return_term loc term = term *)
  51
  52 let fail (x, y) msg =
  53   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
  54
  55 let name_of_string = function
  56   | "_" -> Cic.Anonymous
  57   | s -> Cic.Name s
  58
  59 EXTEND
  60   GLOBAL: term term0;
  61   meta_subst: [
  62     [ s = SYMBOL "_" -> None
  63     | t = term -> Some t ]
  64   ];
  65   binder: [
  66     [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
  67     | SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
  68     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
  69     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
  70   ];
  71   sort: [
  72     [ "Prop" -> `Prop
  73     | "Set" -> `Set
  74     | "Type" -> `Type
  75     | "CProp" -> `CProp ]
  76   ];
  77   typed_name: [
  78     [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
  79         (name_of_string i, Some typ)
  80     | i = IDENT -> (name_of_string i, None)
  81     ]
  82   ];
  83   substituted_name: [ (* a subs.name is an explicit substitution subject *)
  84     [ s = [ IDENT | SYMBOL ];
  85       subst = OPT [
  86         SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
  87         PAREN "[";
  88         substs = LIST1 [
  89           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
  90         ] SEP SYMBOL ";";
  91         PAREN "]" ->
  92           substs
  93       ] ->
  94         (match subst with
  95         | Some l -> CicAst.Ident (s, l)
  96         | None -> CicAst.Ident (s, []))
  97     ]
  98   ];
  99   name: [ (* as substituted_name with no explicit substitution *)
 100     [ s = [ IDENT | SYMBOL ] -> s ]
 101   ];
 102   pattern: [
 103     [ n = name -> (n, [])
 104     | PAREN "("; head = name; vars = LIST1 typed_name; PAREN ")" ->
 105         (head, vars)
 106     ]
 107   ];
 108   term0: [ [ t = term; EOI -> return_term loc t ] ];
 109   term:
 110     [ "binder" RIGHTA
 111       [
 112         b = binder;
 113         (vars, typ) =
 114           [ vars = LIST1 IDENT SEP SYMBOL ",";
 115             typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
 116           | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
 117             typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
 118           ];
 119         SYMBOL "."; body = term ->
 120           let binder =
 121             List.fold_right
 122               (fun var body ->
 123                 let name = name_of_string var in
 124                 CicAst.Binder (b, (name, typ), body))
 125               vars body
 126           in
 127           return_term loc binder
 128       | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
 129             return_term loc
 130               (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
 131       ]
 132     | "eq" LEFTA
 133       [ t1 = term; SYMBOL "="; t2 = term ->
 134         return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
 135       ]
 136     | "add" LEFTA     [ (* nothing here by default *) ]
 137     | "mult" LEFTA    [ (* nothing here by default *) ]
 138     | "inv" NONA      [ (* nothing here by default *) ]
 139     | "simple" NONA
 140       [ sort = sort -> CicAst.Sort sort
 141       | n = substituted_name -> return_term loc n
 142       | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
 143           return_term loc (CicAst.Appl (head :: args))
 144       | i = NUM -> return_term loc (CicAst.Num (i, 0))
 145       | IMPLICIT -> return_term loc CicAst.Implicit
 146       | m = META;
 147         substs = [
 148           PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
 149             substs
 150         ] ->
 151             let index =
 152               try
 153                 int_of_string (String.sub m 1 (String.length m - 1))
 154               with Failure "int_of_string" ->
 155                 fail loc ("Invalid meta variable number: " ^ m)
 156             in
 157             return_term loc (CicAst.Meta (index, substs))
 158         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
 159          * since applications are required to be bound by parens *)
 160       | "let"; var = typed_name;
 161 (*         SYMBOL <:unicode<def>> (* ≝ *); *)
 162         SYMBOL "=";
 163         t1 = term;
 164         IDENT "in"; t2 = term ->
 165           return_term loc (CicAst.LetIn (var, t1, t2))
 166       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 167           defs = LIST1 [
 168             var = typed_name;
 169             index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
 170               int_of_string index
 171             ];
 172 (*             SYMBOL <:unicode<def>> (* ≝ *); *)
 173             SYMBOL "=";
 174             t1 = term ->
 175               (var, t1, (match index with None -> 0 | Some i -> i))
 176           ] SEP (IDENT "and");
 177           IDENT "in"; body = term ->
 178             return_term loc (CicAst.LetRec (ind_kind, defs, body))
 179       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
 180         "match"; t = term;
 181         indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
 182         "with";
 183         PAREN "[";
 184         patterns = LIST0 [
 185           lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term ->
 186             ((lhs: CicAst.case_pattern), rhs)
 187         ] SEP SYMBOL "|";
 188         PAREN "]" ->
 189           return_term loc
 190             (CicAst.Case (t, indty_ident, outtyp, patterns))
 191       | PAREN "("; t = term; PAREN ")" -> return_term loc t
 192       ]
 193     ];
 194 END
 195
 196 let parse_term stream =
 197   try
 198     Grammar.Entry.parse term0 stream
 199   with Stdpp.Exc_located ((x, y), exn) ->
 200     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 201         (Printexc.to_string exn)))
 202
 203 (**/**)
 204
 205 (** {2 Interface for gTopLevel} *)
 206
 207 open DisambiguateTypes
 208
 209 module EnvironmentP3 =
 210   struct
 211     type t = environment
 212
 213     let empty = ""
 214
 215     let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 216     let aliases = Grammar.Entry.create aliases_grammar "aliases"
 217
 218     let to_string env =
 219       let aliases =
 220         Environment.fold
 221           (fun domain_item (dsc, _) acc ->
 222             let s =
 223               match domain_item with
 224               | Id id -> sprintf "alias id %s = %s" id dsc
 225               | Symbol (symb, instance) ->
 226                   sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
 227                     symb instance dsc
 228               | Num instance ->
 229                   sprintf "alias num (instance %d) = \"%s\"" instance dsc
 230             in
 231             s :: acc)
 232           env []
 233       in
 234       String.concat "\n" (List.sort compare aliases)
 235
 236     EXTEND
 237       GLOBAL: aliases;
 238       aliases: [  (* build an environment from an aliases list *)
 239         [ aliases = LIST0 alias; EOI ->
 240             List.fold_left
 241               (fun env (domain_item, codomain_item) ->
 242                 Environment.add domain_item codomain_item env)
 243               Environment.empty aliases
 244         ]
 245       ];
 246       alias: [  (* return a pair <domain_item, codomain_item> from an alias *)
 247         [ IDENT "alias";
 248           choice =
 249             [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI ->
 250                 (Id id, choice_of_uri uri)
 251             | IDENT "symbol"; symbol = QSTRING;
 252               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 253               SYMBOL "="; dsc = QSTRING ->
 254                 (Symbol (symbol, int_of_string instance),
 255                  DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
 256             | IDENT "num";
 257               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 258               SYMBOL "="; dsc = QSTRING ->
 259                 (Num (int_of_string instance),
 260                  DisambiguateChoices.lookup_num_by_dsc dsc)
 261             ] -> choice ]
 262       ];
 263     END
 264
 265     let of_string s =
 266       if s = empty then
 267         Environment.empty
 268       else
 269         try
 270           Grammar.Entry.parse aliases (Stream.of_string s)
 271         with Stdpp.Exc_located ((x, y), exn) ->
 272           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 273           (Printexc.to_string exn)))
 274   end
 275