X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=66037155292c62d75ca540971d7af292daee07eb;hb=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;hp=fcd209307fd73e6c1202e3439a6791ef968d24c2;hpb=935c8d1b73726bb49b99e5c2dbebdea0d617fa1a;p=helm.git diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index fcd209307..660371552 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -63,7 +63,7 @@ let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term ~refresh_uri_in_reference t, n) type binding = - | NoBinding + | NoBinding of string option (* name of Ast.Symbol associated to this literal *) | Binding of string * Env.value_type | Env of (string * Env.value_type) list @@ -189,16 +189,17 @@ let make_action status action bindings = let rec aux (vl : NotationEnv.t) = function [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) - | NoBinding :: tl -> + | NoBinding csym :: tl -> Gramext.action (fun ((*_,*)(loc: Ast.location)) -> let uri,desc = try + let a,b = HExtlib.loc_of_floc loc in CicNotationLexer.LocalizeEnv.find loc !(status#notation_parser_db.loctable) with Not_found -> None, None in aux (("",(Env.NoType, - Env.DisambiguationValue (loc,uri,desc)))::vl) tl) + Env.DisambiguationValue (csym,loc,uri,desc)))::vl) tl) (* LUCA: DEFCON 3 BEGIN *) | Binding (name, Env.TermType l) :: tl -> Gramext.action @@ -231,7 +232,7 @@ let flatten_opt = let rec aux acc = function [] -> List.rev acc - | NoBinding :: tl -> aux acc tl + | NoBinding _ :: tl -> aux acc tl | Env names :: tl -> aux (List.rev names @ acc) tl | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl in @@ -250,12 +251,12 @@ let update_sym_grammar status pattern = assert false and aux_literal status = function - | `Symbol (s,_) -> add_item_to_grammar status (`Sym s) - | `Keyword (s,_) -> + | _,`Symbol (s,_) -> add_item_to_grammar status (`Sym s) + | _,`Keyword (s,_) -> if not (List.mem s CicNotationLexer.initial_keywords) then add_item_to_grammar status (`Kwd s) else status - | `Number _ -> status + | _,`Number _ -> status and aux_layout status = function | Ast.Sub (p1, p2) -> aux (aux status p1) p2 | Ast.Sup (p1, p2) -> aux (aux status p1) p2 @@ -279,7 +280,7 @@ let update_sym_grammar status pattern = | Ast.List0 (p, s) | Ast.List1 (p, s) -> let status = - match s with None -> status | Some s' -> aux_literal status s' + match s with None -> status | Some s' -> aux_literal status (None,s') in aux status p | _ -> assert false @@ -300,24 +301,24 @@ let extract_term_production status pattern = assert false and aux_literal = function - | `Symbol (s,_) -> [NoBinding, gram_symbol status s] - | `Keyword (s,_) -> + | csym,`Symbol (s,_) -> [NoBinding csym, gram_symbol status s] + | csym,`Keyword (s,_) -> (* assumption: s will be registered as a keyword with the lexer *) - [NoBinding, gram_keyword status s] - | `Number (s,_) -> [NoBinding, gram_number s] + [NoBinding csym, gram_keyword status s] + | csym,`Number (s,_) -> [NoBinding csym, gram_number s] and aux_layout = function - | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2 - | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2 - | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2 - | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2 - | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2 - | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3 - | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2 - | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2 + | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sub "] @ aux p2 + | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sup "] @ aux p2 + | Ast.Below (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\below "] @ aux p2 + | Ast.Above (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\above "] @ aux p2 + | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\frac "] @ aux p2 + | Ast.InfRule (p1, p2, p3) -> [NoBinding None, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3 + | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\atop "] @ aux p2 + | Ast.Over (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\over "] @ aux p2 | Ast.Root (p1, p2) -> - [NoBinding, gram_symbol status "\\root "] @ aux p2 - @ [NoBinding, gram_symbol status "\\of "] @ aux p1 - | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p + [NoBinding None, gram_symbol status "\\root "] @ aux p2 + @ [NoBinding None, gram_symbol status "\\of "] @ aux p1 + | Ast.Sqrt p -> [NoBinding None, gram_symbol status "\\sqrt "] @ aux p | Ast.Break -> [] | Ast.Box (_, pl) -> List.flatten (List.map aux pl) | Ast.Group pl -> List.flatten (List.map aux pl) @@ -560,6 +561,14 @@ EXTEND | n = NUMBER -> `Number (n,(None,None)) ] ]; + rliteral: [ + [ csymname = OPT [ "ref" ; csymname = CSYMBOL -> + prerr_endline ("parser in rliteral (ref " ^ csymname ^ ")"); + csymname ]; + lit = literal -> + csymname, lit + ] + ]; sep: [ [ "sep"; sep = literal -> sep ] ]; l1_magic_pattern: [ [ "list0"; p = l1_simple_pattern; sep = OPT sep -> @@ -649,7 +658,7 @@ EXTEND return_term_of_level loc (fun l -> Ast.Magic (m l)) | v = l1_pattern_variable -> return_term_of_level loc (fun _ -> Ast.Variable v) - | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l) + | l = rliteral -> return_term_of_level loc (fun _ -> Ast.Literal l) ] ]; END