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   ];
  72   typed_name: [
  73     [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
  74         (name_of_string i, Some typ)
  75     | i = IDENT -> (name_of_string i, None)
  76     ]
  77   ];
  78   substituted_name: [ (* a subs.name is an explicit substitution subject *)
  79     [ s = [ IDENT | SYMBOL ];
  80       subst = OPT [
  81         SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
  82         PAREN "[";
  83         substs = LIST1 [
  84           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
  85         ] SEP SYMBOL ";";
  86         PAREN "]" ->
  87           substs
  88       ] ->
  89         (match subst with
  90         | Some l -> CicAst.Ident (s, l)
  91         | None -> CicAst.Ident (s, []))
  92     ]
  93   ];
  94   name: [ (* as substituted_name with no explicit substitution *)
  95     [ s = [ IDENT | SYMBOL ] -> s ]
  96   ];
  97   pattern: [
  98     [ n = name -> (n, [])
  99     | PAREN "("; head = name; vars = LIST1 typed_name; PAREN ")" ->
 100         (head, vars)
 101     ]
 102   ];
 103   term0: [ [ t = term -> return_term loc t ] ];
 104   term:
 105     [ "arrow" RIGHTA
 106       [ t1 = term; SYMBOL <:unicode<to>>; t2 = term ->
 107           return_term loc
 108             (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
 109       ]
 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       ]
 129     | "eq" LEFTA
 130       [ t1 = term; SYMBOL "="; t2 = term ->
 131         return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
 132       ]
 133     | "add" LEFTA     [ (* nothing here by default *) ]
 134     | "mult" LEFTA    [ (* nothing here by default *) ]
 135     | "inv" NONA      [ (* nothing here by default *) ]
 136     | "simple" NONA
 137       [
 138         sort_kind = [
 139           "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp
 140         ] ->
 141           CicAst.Sort sort_kind
 142       | n = substituted_name -> return_term loc n
 143       | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
 144           return_term loc (CicAst.Appl (head :: args))
 145       | i = NUM -> return_term loc (CicAst.Num (i, 0))
 146       | IMPLICIT -> return_term loc CicAst.Implicit
 147       | m = META;
 148         substs = [
 149           PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
 150             substs
 151         ] ->
 152             let index =
 153               try
 154                 int_of_string (String.sub m 1 (String.length m - 1))
 155               with Failure "int_of_string" ->
 156                 fail loc ("Invalid meta variable number: " ^ m)
 157             in
 158             return_term loc (CicAst.Meta (index, substs))
 159         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
 160          * since applications are required to be bound by parens *)
 161       | "let"; var = typed_name;
 162 (*         SYMBOL <:unicode<def>> (* ≝ *); *)
 163         SYMBOL "=";
 164         t1 = term;
 165         IDENT "in"; t2 = term ->
 166           return_term loc (CicAst.LetIn (var, t1, t2))
 167       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 168           defs = LIST1 [
 169             var = typed_name;
 170             index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
 171               int_of_string index
 172             ];
 173 (*             SYMBOL <:unicode<def>> (* ≝ *); *)
 174             SYMBOL "=";
 175             t1 = term ->
 176               (var, t1, (match index with None -> 0 | Some i -> i))
 177           ] SEP (IDENT "and");
 178           IDENT "in"; body = term ->
 179             return_term loc (CicAst.LetRec (ind_kind, defs, body))
 180       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
 181         "match"; t = term;
 182         SYMBOL ":"; indty = IDENT;
 183         "with";
 184         PAREN "[";
 185         patterns = LIST0 [
 186           lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term ->
 187             ((lhs: CicAst.case_pattern), rhs)
 188         ] SEP SYMBOL "|";
 189         PAREN "]" ->
 190           return_term loc
 191             (CicAst.Case (t, indty, outtyp, patterns))
 192       | PAREN "("; t = term; PAREN ")" -> return_term loc t
 193       ]
 194     ];
 195 END
 196
 197 let parse_term stream =
 198   try
 199     Grammar.Entry.parse term0 stream
 200   with Stdpp.Exc_located ((x, y), exn) ->
 201     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 202         (Printexc.to_string exn)))
 203
 204 (**/**)
 205
 206 (** {2 Interface for gTopLevel} *)
 207
 208 open DisambiguateTypes
 209
 210 module EnvironmentP3 =
 211   struct
 212     type t = environment
 213
 214     let empty = ""
 215
 216     let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 217     let aliases = Grammar.Entry.create aliases_grammar "aliases"
 218
 219     let to_string env =
 220       let aliases =
 221         Environment.fold
 222           (fun domain_item (dsc, _) acc ->
 223             let s =
 224               match domain_item with
 225               | Id id -> sprintf "alias id %s = %s" id dsc
 226               | Symbol (symb, instance) ->
 227                   sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
 228                     symb instance dsc
 229               | Num instance ->
 230                   sprintf "alias num (instance %d) = \"%s\"" instance dsc
 231             in
 232             s :: acc)
 233           env []
 234       in
 235       String.concat "\n" (List.sort compare aliases)
 236
 237     EXTEND
 238       GLOBAL: aliases;
 239       aliases: [  (* build an environment from an aliases list *)
 240         [ aliases = LIST0 alias; EOI ->
 241             List.fold_left
 242               (fun env (domain_item, codomain_item) ->
 243                 Environment.add domain_item codomain_item env)
 244               Environment.empty aliases
 245         ]
 246       ];
 247       alias: [  (* return a pair <domain_item, codomain_item> from an alias *)
 248         [ IDENT "alias";
 249           choice =
 250             [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI ->
 251                 (Id id, choice_of_uri uri)
 252             | IDENT "symbol"; symbol = QSTRING;
 253               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 254               SYMBOL "="; dsc = QSTRING ->
 255                 (Symbol (symbol, int_of_string instance),
 256                  DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
 257             | IDENT "num";
 258               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 259               SYMBOL "="; dsc = QSTRING ->
 260                 (Num (int_of_string instance),
 261                  DisambiguateChoices.lookup_num_by_dsc dsc)
 262             ] -> choice ]
 263       ];
 264     END
 265
 266     let of_string s =
 267       if s = empty then
 268         Environment.empty
 269       else
 270         try
 271           Grammar.Entry.parse aliases (Stream.of_string s)
 272         with Stdpp.Exc_located ((x, y), exn) ->
 273           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 274           (Printexc.to_string exn)))
 275   end
 276