X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=507d897fbdea8104181ae767e427e3ed9d3b6957;hb=335186953e826833ed43b33cac98884d3f99a228;hp=0ac8ab38072ec67a81e5567412ebafc5604d2180;hpb=d4a5f73930368705b8ce07c11ecff94e04465acb;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 0ac8ab380..507d897fb 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -35,9 +35,14 @@ open Printf exception Parse_error of string -let grammar = Grammar.gcreate CicTextualLexer2.lex +let choice_of_uri (uri: string) = + let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in + (uri, (fun _ _ _ -> cic)) + +let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer let term = Grammar.Entry.create grammar "term" +let term0 = Grammar.Entry.create grammar "term0" (* let tactic = Grammar.Entry.create grammar "tactic" *) (* let tactical = Grammar.Entry.create grammar "tactical" *) @@ -48,7 +53,7 @@ let fail (x, y) msg = failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) EXTEND - GLOBAL: term; + GLOBAL: term term0; meta_subst: [ [ s = SYMBOL "_" -> None | t = term -> Some t ] @@ -64,11 +69,11 @@ EXTEND [ s = [ IDENT | SYMBOL ]; subst = OPT [ SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *) - LPAREN "["; + PAREN "["; substs = LIST1 [ i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) ] SEP SYMBOL ";"; - RPAREN "]" -> + PAREN "]" -> substs ] -> (match subst with @@ -81,22 +86,16 @@ EXTEND ]; pattern: [ [ n = name -> [n] - | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ] + | PAREN "("; names = LIST1 name; PAREN ")" -> names ] ]; + term0: [ [ t = term -> return_term loc t ] ]; term: [ "arrow" RIGHTA [ t1 = term; SYMBOL <:unicode>; t2 = term -> return_term loc (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) ] - | "eq" LEFTA - [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2])) - ] - | "add" LEFTA [ (* nothing here by default *) ] - | "mult" LEFTA [ (* nothing here by default *) ] - | "inv" NONA [ (* nothing here by default *) ] - | "simple" NONA + | "binder" RIGHTA [ b = binder; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; @@ -113,17 +112,27 @@ EXTEND vars body in return_term loc binder - | sort_kind = [ + ] + | "eq" LEFTA + [ t1 = term; SYMBOL "="; t2 = term -> + return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2])) + ] + | "add" LEFTA [ (* nothing here by default *) ] + | "mult" LEFTA [ (* nothing here by default *) ] + | "inv" NONA [ (* nothing here by default *) ] + | "simple" NONA + [ + sort_kind = [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp ] -> CicTextualParser2Ast.Sort sort_kind | n = substituted_name -> return_term loc n - | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> + | PAREN "("; head = term; args = LIST1 term; PAREN ")" -> return_term loc (CicTextualParser2Ast.Appl (head :: args)) | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0)) | m = META; substs = [ - LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> + PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> substs ] -> let index = @@ -135,40 +144,120 @@ EXTEND return_term loc (CicTextualParser2Ast.Meta (index, substs)) (* actually "in" and "and" are _not_ keywords. Parsing works anyway * since applications are required to be bound by parens *) - | "let"; name = IDENT; SYMBOL <:unicode> (* ≝ *); t1 = term; + | "let"; name = IDENT; +(* SYMBOL <:unicode> (* ≝ *); *) + SYMBOL "="; + t1 = term; IDENT "in"; t2 = term -> return_term loc (CicTextualParser2Ast.LetIn (name, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = LIST1 [ - name = IDENT; - index = OPT [ LPAREN "("; index = INT; RPAREN ")" -> - int_of_string index - ]; - typ = OPT [ SYMBOL ":"; typ = term -> typ ]; - SYMBOL <:unicode> (* ≝ *); t1 = term -> - (name, t1, typ, (match index with None -> 1 | Some i -> i)) - ] SEP (IDENT "and"); - IDENT "in"; body = term -> - return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body)) - | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; + name = IDENT; + index = OPT [ PAREN "("; index = NUM; PAREN ")" -> + int_of_string index + ]; + typ = OPT [ SYMBOL ":"; typ = term -> typ ]; +(* SYMBOL <:unicode> (* ≝ *); *) + SYMBOL "="; + t1 = term -> + (name, t1, typ, (match index with None -> 1 | Some i -> i)) + ] SEP (IDENT "and"); + IDENT "in"; body = term -> + return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body)) + | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; SYMBOL ":"; indty = IDENT; "with"; - LPAREN "["; + PAREN "["; patterns = LIST0 [ - p = pattern; SYMBOL <:unicode> (* ⇒ *); t = term -> (p, t) + p = pattern; SYMBOL <:unicode> (* ⇒ *); t = term -> + (p, t) ] SEP SYMBOL "|"; - RPAREN "]" -> - return_term loc (CicTextualParser2Ast.Case (t, indty, outtyp, patterns)) - | LPAREN "("; t = term; RPAREN ")" -> return_term loc t + PAREN "]" -> + return_term loc + (CicTextualParser2Ast.Case (t, indty, outtyp, patterns)) + | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; END let parse_term stream = try - Grammar.Entry.parse term stream + Grammar.Entry.parse term0 stream with Stdpp.Exc_located ((x, y), exn) -> raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y (Printexc.to_string exn))) +(**/**) + +(** {2 Interface for gTopLevel} *) + +open DisambiguateTypes + +module EnvironmentP3 = + struct + type t = environment + + let empty = "" + + let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer + let aliases = Grammar.Entry.create aliases_grammar "aliases" + + let to_string env = + let aliases = + Environment.fold + (fun domain_item (dsc, _) acc -> + let s = + match domain_item with + | Id id -> sprintf "alias id %s = %s" id dsc + | Symbol (symb, instance) -> + sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" + symb instance dsc + | Num instance -> + sprintf "alias num (instance %d) = \"%s\"" instance dsc + in + s :: acc) + env [] + in + String.concat "\n" (List.sort compare aliases) + + EXTEND + GLOBAL: aliases; + aliases: [ (* build an environment from an aliases list *) + [ aliases = LIST0 alias; EOI -> + List.fold_left + (fun env (domain_item, codomain_item) -> + Environment.add domain_item codomain_item env) + Environment.empty aliases + ] + ]; + alias: [ (* return a pair from an alias *) + [ IDENT "alias"; + choice = + [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI -> + (Id id, choice_of_uri uri) + | IDENT "symbol"; symbol = QSTRING; + PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; + SYMBOL "="; dsc = QSTRING -> + (Symbol (symbol, int_of_string instance), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) + | IDENT "num"; + PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; + SYMBOL "="; dsc = QSTRING -> + (Num (int_of_string instance), + DisambiguateChoices.lookup_num_by_dsc dsc) + ] -> choice ] + ]; + END + + let of_string s = + if s = empty then + Environment.empty + else + try + Grammar.Entry.parse aliases (Stream.of_string s) + with Stdpp.Exc_located ((x, y), exn) -> + raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y + (Printexc.to_string exn))) + end +