X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=f4651d6374e0452583be24f117eee5e6794f83aa;hb=57b43a967eaf3b0747350cd775d4301a53af2820;hp=b64fdb5ee425cdeb31146740e999a1981d7bc902;hpb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index b64fdb5ee..f4651d637 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -77,15 +77,17 @@ let int_of_string s = (** {2 Grammar extension} *) -let symbol s = Gramext.Stoken ("SYMBOL", s) -let ident s = Gramext.Stoken ("IDENT", s) -let number s = Gramext.Stoken ("NUMBER", s) +let gram_symbol s = Gramext.Stoken ("SYMBOL", s) +let gram_ident s = Gramext.Stoken ("IDENT", s) +let gram_number s = Gramext.Stoken ("NUMBER", s) +let gram_keyword s = Gramext.Stoken ("", s) +let gram_term = Gramext.Sself -let g_symbol_of_literal = +let gram_of_literal = function - | `Symbol s -> symbol s - | `Keyword s -> ident s - | `Number s -> number s + | `Symbol s -> gram_symbol s + | `Keyword s -> gram_keyword s + | `Number s -> gram_number s type binding = | NoBinding @@ -145,21 +147,23 @@ let extract_term_production pattern = assert false and aux_literal = function - | `Symbol s -> [NoBinding, symbol s] - | `Keyword s -> [NoBinding, ident s] - | `Number s -> [NoBinding, number s] + | `Symbol s -> [NoBinding, gram_symbol s] + | `Keyword s -> + (* assumption: s will be registered as a keyword with the lexer *) + [NoBinding, gram_keyword s] + | `Number s -> [NoBinding, gram_number s] and aux_layout = function - | Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\sub"] @ aux p2 - | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\sup"] @ aux p2 - | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\below"] @ aux p2 - | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\above"] @ aux p2 - | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\frac"] @ aux p2 - | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\atop"] @ aux p2 - | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\over"] @ aux p2 + | Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2 + | Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2 + | Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2 + | Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2 + | Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2 + | Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2 + | Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2 | Root (p1, p2) -> - [NoBinding, symbol "\\root"] @ aux p2 @ [NoBinding, symbol "\\of"] - @ aux p1 - | Sqrt p -> [NoBinding, symbol "\\sqrt"] @ aux p + [NoBinding, gram_symbol "\\root"] @ aux p2 + @ [NoBinding, gram_symbol "\\of"] @ aux p1 + | Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p | Break -> [] | Box (_, pl) -> List.flatten (List.map aux pl) and aux_magic magic = @@ -195,24 +199,24 @@ let extract_term_production pattern = let action (env_list : CicNotationEnv.t list) (loc : location) = CicNotationEnv.coalesce_env p_names env_list in - let g_symbol s = + let gram_of_list s = match magic with | List0 (_, None) -> Gramext.Slist0 s | List1 (_, None) -> Gramext.Slist1 s - | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l) - | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l) + | List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l) + | List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l) | _ -> assert false in [ Env (List.map list_declaration p_names), Gramext.srules - [ [ g_symbol (Gramext.srules [ p_atoms, p_action ]) ], + [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ], Gramext.action action ] ] | _ -> assert false and aux_variable = function - | NumVar s -> [Binding (s, NumType), number ""] - | TermVar s -> [Binding (s, TermType), Gramext.Sself] - | IdentVar s -> [Binding (s, StringType), ident ""] + | NumVar s -> [Binding (s, NumType), gram_number ""] + | TermVar s -> [Binding (s, TermType), gram_term] + | IdentVar s -> [Binding (s, StringType), gram_ident ""] | Ascription (p, s) -> assert false (* TODO *) | FreshVar _ -> assert false and inner_pattern p = @@ -233,6 +237,9 @@ let level_of_int precedence = type rule_id = Token.t Gramext.g_symbol list + (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *) +let owned_keywords = Hashtbl.create 23 + let extend level1_pattern ?(precedence = default_precedence) ?associativity action = @@ -252,9 +259,19 @@ let extend level1_pattern ?(precedence = default_precedence) (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc)) p_bindings) ]]] in - p_atoms - -let delete atoms = Grammar.delete_rule term atoms + let keywords = CicNotationUtil.keywords_of_term level1_pattern in + let rule_id = p_atoms in + List.iter CicNotationLexer.add_level2_ast_keyword keywords; + Hashtbl.add owned_keywords rule_id keywords; (* keywords may be [] *) + rule_id + +let delete rule_id = + let atoms = rule_id in + (try + let keywords = Hashtbl.find owned_keywords rule_id in + List.iter CicNotationLexer.remove_level2_ast_keyword keywords + with Not_found -> assert false); + Grammar.delete_rule term atoms (** {2 Grammar} *) @@ -345,7 +362,7 @@ EXTEND return_term loc (CicNotationUtil.boxify p) | "break" -> return_term loc (Layout Break) (* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *) - | "LPAREN"; p = l1_pattern; "RPAREN" -> + | LPAREN; p = l1_pattern; RPAREN -> return_term loc (CicNotationUtil.boxify p) ] | "simple" NONA @@ -398,9 +415,9 @@ EXTEND (* {{{ Grammar for ast patterns, notation level 2 *) level2_ast: [ [ p = term -> p ] ]; sort: [ - [ IDENT "Prop" -> `Prop - | IDENT "Set" -> `Set - | IDENT "Type" -> `Type + [ "Prop" -> `Prop + | "Set" -> `Set + | "Type" -> `Type ] ]; explicit_subst: [ @@ -459,14 +476,14 @@ EXTEND ] ]; induction_kind: [ - [ IDENT "rec" -> `Inductive - | IDENT "corec" -> `CoInductive + [ "rec" -> `Inductive + | "corec" -> `CoInductive ] ]; let_defs: [ [ defs = LIST1 [ name = bound_name; args = bound_names; - index_name = OPT [ IDENT "on"; id = bound_name -> id ]; + index_name = OPT [ "on"; id = bound_name -> id ]; ty = OPT [ SYMBOL ":" ; p = term -> p ]; SYMBOL <:unicode> (* ≝ *); body = term -> let body = fold_binder `Lambda args body in @@ -495,16 +512,16 @@ EXTEND | Some name -> find_arg name 0 args in (name, ty), body, index - ] SEP IDENT "and" -> + ] SEP "and" -> defs ] ]; term: LEVEL "10" (* let in *) [ "10" NONA - [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); + [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (LetIn (var, p1, p2)) - | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in"; + | "let"; k = induction_kind; defs = let_defs; "in"; body = term -> return_term loc (LetRec (k, defs, body)) ] @@ -539,9 +556,9 @@ EXTEND | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s)) | s = sort -> return_term loc (Sort s) | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ]; - IDENT "match"; t = term; + "match"; t = term; indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; - IDENT "with"; SYMBOL "["; + "with"; SYMBOL "["; patterns = LIST0 [ lhs = match_pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term -> @@ -583,7 +600,7 @@ EXTEND ] ]; precedence: [ - [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] + [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] ]; notation: [ [ s = QSTRING; @@ -611,6 +628,7 @@ EXTEND | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." -> Interpretation ((symbol, args), l3) | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u) + | IDENT "dump"; SYMBOL "." -> Dump ] ]; (* }}} *)