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     [ "letin" NONA
 123         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
 124          * since applications are required to be bound by parens *)
 125       [ "let"; var = typed_name;
 126         SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
 127         t1 = term;
 128         IDENT "in"; t2 = term ->
 129           return_term loc (CicAst.LetIn (var, t1, t2))
 130       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 131           defs = LIST1 [
 132             var = typed_name;
 133             index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
 134               int_of_string index
 135             ];
 136             SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
 137             t1 = term ->
 138               (var, t1, (match index with None -> 0 | Some i -> i))
 139           ] SEP (IDENT "and");
 140           IDENT "in"; body = term ->
 141             return_term loc (CicAst.LetRec (ind_kind, defs, body))
 142       ]
 143     | "binder" RIGHTA
 144       [
 145         b = binder;
 146         (vars, typ) =
 147           [ vars = LIST1 IDENT SEP SYMBOL ",";
 148             typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
 149           | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
 150             typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
 151           ];
 152         SYMBOL "."; body = term ->
 153           let binder =
 154             List.fold_right
 155               (fun var body ->
 156                 let name = name_of_string var in
 157                 CicAst.Binder (b, (name, typ), body))
 158               vars body
 159           in
 160           return_term loc binder
 161       | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
 162             return_term loc
 163               (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
 164       ]
 165     | "relop" LEFTA
 166       [ t1 = term; SYMBOL "="; t2 = term ->
 167         return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
 168       ]
 169     | "add" LEFTA     [ (* nothing here by default *) ]
 170     | "mult" LEFTA    [ (* nothing here by default *) ]
 171     | "inv" NONA      [ (* nothing here by default *) ]
 172     | "simple" NONA
 173       [ sort = sort -> CicAst.Sort sort
 174       | n = substituted_name -> return_term loc n
 175       | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
 176           return_term loc (CicAst.Appl (head :: args))
 177       | i = NUM -> return_term loc (CicAst.Num (i, 0))
 178       | IMPLICIT -> return_term loc CicAst.Implicit
 179       | m = META;
 180         substs = [
 181           PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
 182             substs
 183         ] ->
 184             let index =
 185               try
 186                 int_of_string (String.sub m 1 (String.length m - 1))
 187               with Failure "int_of_string" ->
 188                 fail loc ("Invalid meta variable number: " ^ m)
 189             in
 190             return_term loc (CicAst.Meta (index, substs))
 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 [ IDENT "in"; ident = IDENT -> ident ] -> where ]
 208   ];
 209   tactic_term: [ [ t = term -> t ] ];
 210   ident_list0: [
 211     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
 212   ];
 213   ident_list1: [
 214     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
 215   ];
 216   reduction_kind: [
 217     [ "reduce" -> `Reduce
 218     | "simpl" -> `Simpl
 219     | "whd" -> `Whd ]
 220   ];
 221   tactic: [
 222     [ IDENT "absurd" -> return_tactic loc TacticAst.Absurd
 223     | IDENT "apply"; t = tactic_term -> return_tactic loc (TacticAst.Apply t)
 224     | IDENT "assumption" -> return_tactic loc TacticAst.Assumption
 225     | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term;
 226       where = tactic_where ->
 227         return_tactic loc (TacticAst.Change (t1, t2, where))
 228     (* TODO Change_pattern *)
 229     | IDENT "contradiction" -> return_tactic loc TacticAst.Contradiction
 230     | IDENT "cut"; t = tactic_term -> return_tactic loc (TacticAst.Cut t)
 231     | IDENT "decompose"; principles = ident_list1; where = IDENT ->
 232         return_tactic loc (TacticAst.Decompose (where, principles))
 233     | IDENT "discriminate"; hyp = IDENT ->
 234         return_tactic loc (TacticAst.Discriminate hyp)
 235     | IDENT "elim"; IDENT "type"; t = tactic_term ->
 236         return_tactic loc (TacticAst.ElimType t)
 237     | IDENT "elim"; t1 = tactic_term;
 238       using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
 239         return_tactic loc (TacticAst.Elim (t1, using))
 240     | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
 241     | IDENT "exists" -> return_tactic loc TacticAst.Exists
 242     | IDENT "fold"; kind = reduction_kind; t = tactic_term ->
 243         return_tactic loc (TacticAst.Fold (kind, t))
 244     | IDENT "fourier" -> return_tactic loc TacticAst.Fourier
 245     | IDENT "injection"; ident = IDENT ->
 246         return_tactic loc (TacticAst.Injection ident)
 247     | IDENT "intros";
 248       num = OPT [ num = int -> num ];
 249       idents = OPT ident_list0 ->
 250         let idents = match idents with None -> [] | Some idents -> idents in
 251         return_tactic loc (TacticAst.Intros (num, idents))
 252     | IDENT "left" -> return_tactic loc TacticAst.Left
 253     | "let"; t = tactic_term; IDENT "in"; where = IDENT ->
 254         return_tactic loc (TacticAst.LetIn (t, where))
 255     (* TODO Reduce *)
 256     | IDENT "reflexivity" -> return_tactic loc TacticAst.Reflexivity
 257     | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term ->
 258         return_tactic loc (TacticAst.Replace (t1, t2))
 259     (* TODO Rewrite *)
 260     (* TODO Replace_pattern *)
 261     | IDENT "right" -> return_tactic loc TacticAst.Right
 262     | IDENT "ring" -> return_tactic loc TacticAst.Ring
 263     | IDENT "split" -> return_tactic loc TacticAst.Split
 264     | IDENT "symmetry" -> return_tactic loc TacticAst.Symmetry
 265     | IDENT "transitivity"; t = tactic_term ->
 266         return_tactic loc (TacticAst.Transitivity t)
 267     ]
 268   ];
 269   tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
 270   tactical:
 271     [ "sequence" LEFTA
 272       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
 273           return_tactical loc (TacticAst.Seq tactics)
 274       ]
 275     | "then" NONA
 276       [ tac = tactical;
 277         PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
 278           return_tactical loc (TacticAst.Then (tac, tacs))
 279       ]
 280     | "loops" RIGHTA
 281       [ IDENT "do"; count = int; tac = tactical ->
 282           return_tactical loc (TacticAst.Do (count, tac))
 283       | IDENT "repeat"; tac = tactical ->
 284           return_tactical loc (TacticAst.Repeat tac)
 285       ]
 286     | "simple" NONA
 287       [ IDENT "tries";
 288         PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
 289           return_tactical loc (TacticAst.Tries tacs)
 290       | IDENT "try"; tac = NEXT -> return_tactical loc (TacticAst.Try tac)
 291       | IDENT "fail" -> return_tactical loc TacticAst.Fail
 292       | IDENT "id" -> return_tactical loc TacticAst.IdTac
 293       | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
 294       | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
 295       ]
 296     ];
 297 END
 298
 299 let parse_term stream =
 300   try
 301     Grammar.Entry.parse term0 stream
 302   with Stdpp.Exc_located ((x, y), exn) ->
 303     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 304         (Printexc.to_string exn)))
 305
 306 let parse_tactic stream =
 307   try
 308     Grammar.Entry.parse tactic stream
 309   with Stdpp.Exc_located ((x, y), exn) ->
 310     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 311         (Printexc.to_string exn)))
 312
 313 let parse_tactical stream =
 314   try
 315     Grammar.Entry.parse tactical0 stream
 316   with Stdpp.Exc_located ((x, y), exn) ->
 317     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 318         (Printexc.to_string exn)))
 319
 320 (**/**)
 321
 322 (** {2 Interface for gTopLevel} *)
 323
 324 open DisambiguateTypes
 325
 326 module EnvironmentP3 =
 327   struct
 328     type t = environment
 329
 330     let empty = ""
 331
 332     let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 333     let aliases = Grammar.Entry.create aliases_grammar "aliases"
 334
 335     let to_string env =
 336       let aliases =
 337         Environment.fold
 338           (fun domain_item (dsc, _) acc ->
 339             let s =
 340               match domain_item with
 341               | Id id -> sprintf "alias id %s = %s" id dsc
 342               | Symbol (symb, instance) ->
 343                   sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
 344                     symb instance dsc
 345               | Num instance ->
 346                   sprintf "alias num (instance %d) = \"%s\"" instance dsc
 347             in
 348             s :: acc)
 349           env []
 350       in
 351       String.concat "\n" (List.sort compare aliases)
 352
 353     EXTEND
 354       GLOBAL: aliases;
 355       aliases: [  (* build an environment from an aliases list *)
 356         [ aliases = LIST0 alias; EOI ->
 357             List.fold_left
 358               (fun env (domain_item, codomain_item) ->
 359                 Environment.add domain_item codomain_item env)
 360               Environment.empty aliases
 361         ]
 362       ];
 363       alias: [  (* return a pair <domain_item, codomain_item> from an alias *)
 364         [ IDENT "alias";
 365           choice =
 366             [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI ->
 367                 (Id id, choice_of_uri uri)
 368             | IDENT "symbol"; symbol = QSTRING;
 369               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 370               SYMBOL "="; dsc = QSTRING ->
 371                 (Symbol (symbol, int_of_string instance),
 372                  DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
 373             | IDENT "num";
 374               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
 375               SYMBOL "="; dsc = QSTRING ->
 376                 (Num (int_of_string instance),
 377                  DisambiguateChoices.lookup_num_by_dsc dsc)
 378             ] -> choice ]
 379       ];
 380     END
 381
 382     let of_string s =
 383       if s = empty then
 384         Environment.empty
 385       else
 386         try
 387           Grammar.Entry.parse aliases (Stream.of_string s)
 388         with Stdpp.Exc_located ((x, y), exn) ->
 389           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
 390           (Printexc.to_string exn)))
 391   end
 392