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