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 let tactical0 = Grammar.Entry.create grammar "tactical0"
  49
  50 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
  51 let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
  52 let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
  53
  54 let fail (x, y) msg =
  55   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
  56
  57 let name_of_string = function
  58   | "_" -> Cic.Anonymous
  59   | s -> Cic.Name s
  60
  61 EXTEND
  62   GLOBAL: term term0 tactic tactical tactical0;
  63   int: [
  64     [ num = NUM ->
  65         try
  66           int_of_string num
  67         with Failure _ ->
  68           let (x, y) = loc in
  69           raise (Parse_error (sprintf
  70             "integer literal expected at characters %d-%d" x y))
  71     ]
  72   ];
  73   meta_subst: [
  74     [ s = SYMBOL "_" -> None
  75     | t = term -> Some t ]
  76   ];
  77   binder: [
  78     [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
  79     | SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
  80     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
  81     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
  82   ];
  83   sort: [
  84     [ "Prop" -> `Prop
  85     | "Set" -> `Set
  86     | "Type" -> `Type
  87     | "CProp" -> `CProp ]
  88   ];
  89   typed_name: [
  90     [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
  91         (name_of_string i, Some typ)
  92     | i = IDENT -> (name_of_string i, None)
  93     ]
  94   ];
  95   substituted_name: [ (* a subs.name is an explicit substitution subject *)
  96     [ s = [ IDENT | SYMBOL ];
  97       subst = OPT [
  98         SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
  99         PAREN "[";
 100         substs = LIST1 [
 101           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
 102         ] SEP SYMBOL ";";
 103         PAREN "]" ->
 104           substs
 105       ] ->
 106         (match subst with
 107         | Some l -> CicAst.Ident (s, l)
 108         | None -> CicAst.Ident (s, []))
 109     ]
 110   ];
 111   name: [ (* as substituted_name with no explicit substitution *)
 112     [ s = [ IDENT | SYMBOL ] -> s ]
 113   ];
 114   pattern: [
 115     [ n = name -> (n, [])
 116     | PAREN "("; head = name; vars = LIST1 typed_name; PAREN ")" ->
 117         (head, vars)
 118     ]
 119   ];
 120   term0: [ [ t = term; EOI -> return_term loc t ] ];
 121   term:
 122     [ "binder" RIGHTA
 123       [
 124         b = binder;
 125         (vars, typ) =
 126           [ vars = LIST1 IDENT SEP SYMBOL ",";
 127             typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
 128           | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
 129             typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
 130           ];
 131         SYMBOL "."; body = term ->
 132           let binder =
 133             List.fold_right
 134               (fun var body ->
 135                 let name = name_of_string var in
 136                 CicAst.Binder (b, (name, typ), body))
 137               vars body
 138           in
 139           return_term loc binder
 140       | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
 141             return_term loc
 142               (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
 143       ]
 144     | "eq" LEFTA
 145       [ t1 = term; SYMBOL "="; t2 = term ->
 146         return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
 147       ]
 148     | "add" LEFTA     [ (* nothing here by default *) ]
 149     | "mult" LEFTA    [ (* nothing here by default *) ]
 150     | "inv" NONA      [ (* nothing here by default *) ]
 151     | "simple" NONA
 152       [ sort = sort -> CicAst.Sort sort
 153       | n = substituted_name -> return_term loc n
 154       | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
 155           return_term loc (CicAst.Appl (head :: args))
 156       | i = NUM -> return_term loc (CicAst.Num (i, 0))
 157       | IMPLICIT -> return_term loc CicAst.Implicit
 158       | m = META;
 159         substs = [
 160           PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
 161             substs
 162         ] ->
 163             let index =
 164               try
 165                 int_of_string (String.sub m 1 (String.length m - 1))
 166               with Failure "int_of_string" ->
 167                 fail loc ("Invalid meta variable number: " ^ m)
 168             in
 169             return_term loc (CicAst.Meta (index, substs))
 170         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
 171          * since applications are required to be bound by parens *)
 172       | "let"; var = typed_name;
 173 (*         SYMBOL <:unicode<def>> (* ≝ *); *)
 174         SYMBOL "=";
 175         t1 = term;
 176         IDENT "in"; t2 = term ->
 177           return_term loc (CicAst.LetIn (var, t1, t2))
 178       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 179           defs = LIST1 [
 180             var = typed_name;
 181             index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
 182               int_of_string index
 183             ];
 184 (*             SYMBOL <:unicode<def>> (* ≝ *); *)
 185             SYMBOL "=";
 186             t1 = term ->
 187               (var, t1, (match index with None -> 0 | Some i -> i))
 188           ] SEP (IDENT "and");
 189           IDENT "in"; body = term ->
 190             return_term loc (CicAst.LetRec (ind_kind, defs, body))
 191       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
 192         "match"; t = term;
 193         indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
 194         "with";
 195         PAREN "[";
 196         patterns = LIST0 [
 197           lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term ->
 198             ((lhs: CicAst.case_pattern), rhs)
 199         ] SEP SYMBOL "|";
 200         PAREN "]" ->
 201           return_term loc
 202             (CicAst.Case (t, indty_ident, outtyp, patterns))
 203       | PAREN "("; t = term; PAREN ")" -> return_term loc t
 204       ]
 205     ];
 206   tactic_where: [
 207     [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
 208   ];
 209   tactic_term: [
 210     [ t = term -> t ]
 211   ];
 212   ident_list0: [
 213     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
 214   ];
 215   ident_list1: [
 216     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
 217   ];
 218   reduction_kind: [
 219     [ "reduce" -> `Reduce
 220     | "simpl" -> `Simpl
 221     | "whd" -> `Whd ]
 222   ];
 223   tactic: [
 224     [ IDENT "absurd" -> return_tactic loc TacticAst.Absurd
 225     | IDENT "apply"; t = tactic_term -> return_tactic loc (TacticAst.Apply t)
 226     | IDENT "assumption" -> return_tactic loc TacticAst.Assumption
 227     | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term;
 228       where = tactic_where ->
 229         return_tactic loc (TacticAst.Change (t1, t2, where))
 230     (* TODO Change_pattern *)
 231     | IDENT "contradiction" -> return_tactic loc TacticAst.Contradiction
 232     | IDENT "cut"; t = tactic_term -> return_tactic loc (TacticAst.Cut t)
 233     | IDENT "decompose"; principles = ident_list1; where = IDENT ->
 234         return_tactic loc (TacticAst.Decompose (where, principles))
 235     | IDENT "discriminate"; hyp = IDENT ->
 236         return_tactic loc (TacticAst.Discriminate hyp)
 237     | IDENT "elim"; IDENT "type"; t = tactic_term ->
 238         return_tactic loc (TacticAst.ElimType t)
 239     | IDENT "elim"; t1 = tactic_term;
 240       using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
 241         return_tactic loc (TacticAst.Elim (t1, using))
 242     | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
 243     | IDENT "exists" -> return_tactic loc TacticAst.Exists
 244     | IDENT "fold"; kind = reduction_kind; t = tactic_term ->
 245         return_tactic loc (TacticAst.Fold (kind, t))
 246     | IDENT "fourier" -> return_tactic loc TacticAst.Fourier
 247     | IDENT "injection"; ident = IDENT ->
 248         return_tactic loc (TacticAst.Injection ident)
 249     | IDENT "intros";
 250       num = OPT [ num = int -> num ];
 251       idents = OPT ident_list0 ->
 252         let idents = match idents with None -> [] | Some idents -> idents in
 253         return_tactic loc (TacticAst.Intros (num, idents))
 254     | IDENT "left" -> return_tactic loc TacticAst.Left
 255     | "let"; t = tactic_term; IDENT "in"; where = IDENT ->
 256         return_tactic loc (TacticAst.LetIn (t, where))
 257     (* TODO Reduce *)
 258     | IDENT "reflexivity" -> return_tactic loc TacticAst.Reflexivity
 259     | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term ->
 260         return_tactic loc (TacticAst.Replace (t1, t2))
 261     (* TODO Rewrite *)
 262     (* TODO Replace_pattern *)
 263     | IDENT "right" -> return_tactic loc TacticAst.Right
 264     | IDENT "ring" -> return_tactic loc TacticAst.Ring
 265     | IDENT "split" -> return_tactic loc TacticAst.Split
 266     | IDENT "symmetry" -> return_tactic loc TacticAst.Symmetry
 267     | IDENT "transitivity"; t = tactic_term ->
 268         return_tactic loc (TacticAst.Transitivity t)
 269     ]
 270   ];
 271   tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
 272   tactical: [
 273     [ IDENT "fail" -> return_tactical loc TacticAst.Fail
 274     | IDENT "do"; count = int; tac = tactical ->
 275         return_tactical loc (TacticAst.Do (count, tac))
 276     | IDENT "id" -> return_tactical loc TacticAst.IdTac
 277     | IDENT "repeat"; tac = tactical ->
 278         return_tactical loc (TacticAst.Repeat tac)
 279     | tactics = LIST0 tactical SEP SYMBOL ";" ->
 280         return_tactical loc (TacticAst.Seq tactics)
 281     | tac = tactical;
 282       PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
 283         return_tactical loc (TacticAst.Then (tac, tacs))
 284     | IDENT "tries";
 285       PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
 286         return_tactical loc (TacticAst.Tries tacs)
 287     | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac)
 288     | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
 289     | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
 290     ]
 291   ];
 292 END
 293
 294 let parse_term stream =
 295   try
 296     Grammar.Entry.parse term0 stream
 297   with Stdpp.Exc_located ((x, y), exn) ->
 298     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 299         (Printexc.to_string exn)))
 300
 301 let parse_tactic stream =
 302   try
 303     Grammar.Entry.parse tactic stream
 304   with Stdpp.Exc_located ((x, y), exn) ->
 305     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 306         (Printexc.to_string exn)))
 307
 308 let parse_tactical stream =
 309   try
 310     Grammar.Entry.parse tactical0 stream
 311   with Stdpp.Exc_located ((x, y), exn) ->
 312     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 313         (Printexc.to_string exn)))
 314
 315 (**/**)
 316
 317 (** {2 Interface for gTopLevel} *)
 318
 319 open DisambiguateTypes
 320
 321 module EnvironmentP3 =
 322   struct
 323     type t = environment
 324
 325     let empty = ""
 326
 327     let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 328     let aliases = Grammar.Entry.create aliases_grammar "aliases"
 329
 330     let to_string env =
 331       let aliases =
 332         Environment.fold
 333           (fun domain_item (dsc, _) acc ->
 334             let s =
 335               match domain_item with
 336               | Id id -> sprintf "alias id %s = %s" id dsc
 337               | Symbol (symb, instance) ->
 338                   sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
 339                     symb instance dsc
 340               | Num instance ->
 341                   sprintf "alias num (instance %d) = \"%s\"" instance dsc
 342             in
 343             s :: acc)
 344           env []
 345       in
 346       String.concat "\n" (List.sort compare aliases)
 347
 348     EXTEND
 349       GLOBAL: aliases;
 350       aliases: [  (* build an environment from an aliases list *)
 351         [ aliases = LIST0 alias; EOI ->
 352             List.fold_left
 353               (fun env (domain_item, codomain_item) ->
 354                 Environment.add domain_item codomain_item env)
 355               Environment.empty aliases
 356         ]
 357       ];
 358       alias: [  (* return a pair <domain_item, codomain_item> from an alias *)
 359         [ IDENT "alias";
 360           choice =
 361             [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI ->
 362                 (Id id, choice_of_uri uri)
 363             | IDENT "symbol"; symbol = QSTRING;
 364               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 365               SYMBOL "="; dsc = QSTRING ->
 366                 (Symbol (symbol, int_of_string instance),
 367                  DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
 368             | IDENT "num";
 369               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 370               SYMBOL "="; dsc = QSTRING ->
 371                 (Num (int_of_string instance),
 372                  DisambiguateChoices.lookup_num_by_dsc dsc)
 373             ] -> choice ]
 374       ];
 375     END
 376
 377     let of_string s =
 378       if s = empty then
 379         Environment.empty
 380       else
 381         try
 382           Grammar.Entry.parse aliases (Stream.of_string s)
 383         with Stdpp.Exc_located ((x, y), exn) ->
 384           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 385           (Printexc.to_string exn)))
 386   end
 387