level2_ast_grammar : Grammar.g;
term: 'b Grammar.Entry.e;
ident: 'e Grammar.Entry.e;
+ sym_attributes: (string option * string option) Grammar.Entry.e;
+ sym_table: (string * Stdpp.location Grammar.Entry.e) list;
let_defs: 'c Grammar.Entry.e;
protected_binder_vars: 'd Grammar.Entry.e;
level2_meta: 'b Grammar.Entry.e;
Ast.term Ast.capture_variable * Ast.term * int) list,
Ast.term list * Ast.term option, Env.ident_or_var) grammars;
keywords: string list;
- items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list
+ items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list;
+ loctable: (string option * string option) CicNotationLexer.LocalizeEnv.t ref
}
let int_of_string s =
raise (Level_not_found precedence);
string_of_int precedence
-let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
+let add_symbol_to_grammar_explicit level2_ast_grammar
+ sym_attributes sym_table s =
+ try
+ let _ = List.assoc s sym_table
+ in sym_table
+ with Not_found ->
+ let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) in
+ Grammar.extend
+ [ Grammar.Entry.obj entry,
+ None,
+ [ None,
+ Some (*Gramext.NonA*) Gramext.NonA,
+ [ [Gramext.Stoken ("SYMBOL",s)], (* concrete l1 syntax *)
+ (Gramext.action (fun _ loc -> None, loc))
+ ; [Gramext.Stoken ("ATAG","")
+ ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
+ ;Gramext.Stoken ("SYMBOL","\005")
+ ;Gramext.Stoken ("SYMBOL",s)
+ ;Gramext.Stoken ("ATAGEND","")],
+ (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
+ ]]];
+(* prerr_endline ("adding to grammar symbol " ^ s); *)
+ (s,entry)::sym_table
+
+
+let add_symbol_to_grammar status s =
+ let sym_attributes = status#notation_parser_db.grammars.sym_attributes in
+ let sym_table = status#notation_parser_db.grammars.sym_table in
+ let level2_ast_grammar =
+ status#notation_parser_db.grammars.level2_ast_grammar
+ in
+ let sym_table =
+ add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes sym_table s
+ in
+ let grammars =
+ { status#notation_parser_db.grammars with sym_table = sym_table }
+ in
+ let notation_parser_db =
+ { status#notation_parser_db with grammars = grammars } in
+ status#set_notation_parser_db notation_parser_db
+
+let gram_symbol status s =
+ let sym_table = status#notation_parser_db.grammars.sym_table in
+ let entry =
+ try List.assoc s sym_table
+ with Not_found ->
+ (let syms = List.map fst (status#notation_parser_db.grammars.sym_table) in
+ let syms = List.map (fun x -> "\"" ^ x ^ "\"") syms in
+ prerr_endline ("new symbol non-terminals: " ^ (String.concat ", " syms));
+ prerr_endline ("unable to find symbol \"" ^ s ^ "\""); assert false)
+ in
+ Gramext.Snterm (Grammar.Entry.obj entry)
+
let gram_ident status =
Gramext.Snterm (Grammar.Entry.obj
(status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
level_of precedence)
;;
-let gram_of_literal =
+let gram_of_literal status =
function
- | `Symbol s -> gram_symbol s
- | `Keyword s -> gram_keyword s
- | `Number s -> gram_number s
+ | `Symbol (s,_) -> gram_symbol status s
+ | `Keyword (s,_) -> gram_keyword s
+ | `Number (s,_) -> gram_number s
-let make_action action bindings =
+let make_action status action bindings =
let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
- | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
+ | NoBinding :: tl ->
+ Gramext.action
+ (fun (_,(loc: Ast.location)) ->
+ let uri,desc =
+ try
+ 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)
(* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType l) :: tl ->
Gramext.action
aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
| Env _ :: tl ->
Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl)
+ | _ (* Binding (_,NoType) *) -> assert false
(* LUCA: DEFCON 3 END *)
in
aux [] (List.rev bindings)
in
aux []
+(* given a level 1 pattern, adds productions for symbols when needed *)
+let update_sym_grammar status pattern =
+ let rec aux status = function
+ | Ast.AttributedTerm (_, t) -> aux status t
+ | Ast.Literal l -> aux_literal status l
+ | Ast.Layout l -> aux_layout status l
+ | Ast.Magic m -> aux_magic status m
+ | Ast.Variable v -> aux_variable status v
+ | t ->
+ prerr_endline (NotationPp.pp_term status t);
+ assert false
+ and aux_literal status =
+ function
+ | `Symbol (s,_) -> add_symbol_to_grammar status s
+ | `Keyword _ -> 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
+ | Ast.Below (p1, p2) -> aux (aux status p1) p2
+ | Ast.Above (p1, p2) -> aux (aux status p1) p2
+ | Ast.Frac (p1, p2) -> aux (aux status p1) p2
+ | Ast.InfRule (p1, p2, p3) -> aux (aux (aux status p1) p2) p3
+ | Ast.Atop (p1, p2) -> aux (aux status p1) p2
+ | Ast.Over (p1, p2) -> aux (aux status p1) p2
+ | Ast.Root (p1, p2) -> aux (aux status p1) p2
+ | Ast.Sqrt p -> aux status p
+ | Ast.Break -> status
+ | Ast.Box (_, pl) -> List.fold_left aux status pl
+ | Ast.Group pl -> List.fold_left aux status pl
+ | Ast.Mstyle (_,pl) -> List.fold_left aux status pl
+ | Ast.Mpadded (_,pl) -> List.fold_left aux status pl
+ | Ast.Maction l -> List.fold_left aux status l
+ and aux_magic status magic =
+ match magic with
+ | Ast.Opt p -> aux status p
+ | Ast.List0 (p, s)
+ | Ast.List1 (p, s) ->
+ let status =
+ match s with None -> status | Some s' -> aux_literal status s'
+ in
+ aux status p
+ | _ -> assert false
+ and aux_variable status _ = status
+ in
+ aux status pattern
+
(* given a level 1 pattern computes the new RHS of "term" grammar entry *)
let extract_term_production status pattern =
let rec aux = function
assert false
and aux_literal =
function
- | `Symbol s -> [NoBinding, gram_symbol s]
- | `Keyword s ->
+ | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
+ | `Keyword (s,_) ->
(* assumption: s will be registered as a keyword with the lexer *)
[NoBinding, gram_keyword s]
- | `Number s -> [NoBinding, gram_number s]
+ | `Number (s,_) -> [NoBinding, gram_number s]
and aux_layout = function
- | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2
- | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2
- | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below "] @ aux p2
- | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above "] @ aux p2
- | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac "] @ aux p2
- | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule "] @ aux p1 @ aux p2 @ aux p3
- | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop "] @ aux p2
- | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over "] @ aux p2
+ | 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.Root (p1, p2) ->
- [NoBinding, gram_symbol "\\root "] @ aux p2
- @ [NoBinding, gram_symbol "\\of "] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p
+ [NoBinding, gram_symbol status "\\root "] @ aux p2
+ @ [NoBinding, gram_symbol status "\\of "] @ aux p1
+ | Ast.Sqrt p -> [NoBinding, 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)
match magic with
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) ->
+ Gramext.Slist0sep (s, gram_of_literal status l)
+ | Ast.List1 (_, Some l) ->
+ Gramext.Slist1sep (s, gram_of_literal status l)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
let p_bindings, p_atoms = List.split (aux p) in
let p_names = flatten_opt p_bindings in
let action =
- make_action (fun (env : NotationEnv.t) (loc : Ast.location) -> env)
- p_bindings
+ make_action status
+ (fun (env : NotationEnv.t) (loc : Ast.location) -> env) p_bindings
in
p_bindings, p_atoms, p_names, action
in
let parse_level2_ast grammars lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse grammars.level2_ast (Obj.magic lexbuf))
+ (fun () ->
+ Grammar.Entry.parse grammars.level2_ast (Obj.magic lexbuf))
let parse_level2_meta grammars lexbuf =
exc_located_wrapper
(fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf))
(* create empty precedence level for "term" *)
-let initialize_grammars grammars =
+let initialize_grammars loctable grammars =
let dummy_action =
Gramext.action (fun _ ->
failwith "internal error, lexer generated a dummy token")
fun l -> List.map (fun x -> x l) p ]
];
literal: [
- [ s = SYMBOL -> `Symbol s
- | k = QKEYWORD -> `Keyword k
- | n = NUMBER -> `Number n
+ [ s = SYMBOL -> `Symbol (s, (None,None))
+ | k = QKEYWORD -> `Keyword (k, (None,None))
+ | n = NUMBER -> `Number (n,(None,None))
]
];
sep: [ [ "sep"; sep = literal -> sep ] ];
begin
let level2_ast = grammars.level2_ast in
let term = grammars.term in
+ let atag_attributes = grammars.sym_attributes in
let let_defs = grammars.let_defs in
let ident = grammars.ident in
let protected_binder_vars = grammars.protected_binder_vars in
EXTEND
- GLOBAL: level2_ast term let_defs protected_binder_vars ident;
+ GLOBAL: level2_ast term let_defs protected_binder_vars ident atag_attributes;
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
| "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
]
];
- explicit_subst: [
- [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *)
- SYMBOL "[";
- substs = LIST1 [
- i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
- ] SEP SYMBOL ";";
- SYMBOL "]" ->
- substs
- ]
- ];
meta_subst: [
[ s = SYMBOL "_" -> None
| p = term -> Some p ]
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
];
+ gident: [
+ [ id = IDENT ->
+ try
+ let uri,_ = CicNotationLexer.LocalizeEnv.find loc
+ !loctable in
+ match uri with
+ | Some u ->
+ prerr_endline ("trovata interpretazione per " ^ id ^ ": " ^ u);
+ id, `Uri u
+ | None ->
+ prerr_endline ("identificatore ambiguo: " ^ id);
+ id, `Ambiguous
+ with
+ | Not_found ->
+ prerr_endline ("identificatore non trovato: " ^ id);
+ id, `Ambiguous ]];
+ gnum: [
+ [ n = NUMBER ->
+ try
+ match CicNotationLexer.LocalizeEnv.find loc !loctable with
+ | _uri, Some interpr -> n, Some (Some "cic:/fakeuri.def(1)",interpr)
+ | _ -> n,None
+ with
+ | Not_found -> n,None ]];
arg: [
- [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
+ [ LPAREN; names = LIST1 gident SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
- List.map (fun n -> Ast.Ident (n, `Ambiguous)) names, Some ty
- | name = IDENT -> [Ast.Ident (name, `Ambiguous)], None
+ List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty
+ | (name,uri) = gident -> [Ast.Ident (name,uri)], None
| blob = UNPARSED_META ->
let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
match meta with
]
];
single_arg: [
- [ name = IDENT -> Ast.Ident (name, `Ambiguous)
+ [ (name,uri) = gident -> Ast.Ident (name,uri)
| blob = UNPARSED_META ->
let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
match meta with
(* CSC: new NCicPp.status is the best I can do here
without changing the return type *)
Ast.fail loc (sprintf "Argument %s not found"
- (NotationPp.pp_term (new NCicPp.status) name))
+ (NotationPp.pp_term (new NCicPp.status None) name))
| (l,_) :: tl ->
(match position_of name 0 l with
| None, len -> find_arg name (n + len) tl
var =
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
- | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
- Ast.Ident(id,`Ambiguous), ty ];
+ | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
+ Ast.Ident (id,uri), ty ];
SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
];
term: LEVEL "90"
[
- [ id = IDENT -> return_term loc (Ast.Ident (id, `Ambiguous))
- | id = IDENT; s = explicit_subst -> (* XXX: no more explicit subst? *)
- assert false
- (* return_term loc (Ast.Ident (id, Some s))*)
+ [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri))
| s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
| u = URI -> return_term loc (Ast.Ident
(NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
| r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
- | n = NUMBER -> return_term loc (Ast.Num (n, None))
+ | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr))
| IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
| SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
| PLACEHOLDER -> return_term loc Ast.UserInput
grammars
;;
-let initial_grammars keywords =
- let lexers = CicNotationLexer.mk_lexers keywords in
+let initial_grammars loctable keywords =
+ let lexers = CicNotationLexer.mk_lexers loctable keywords in
let level1_pattern_grammar =
Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in
let level2_ast_grammar =
let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
let term = Grammar.Entry.create level2_ast_grammar "term" in
let ident = Grammar.Entry.create level2_ast_grammar "ident" in
+ (* unexpanded TeX macros terminated by a space (see comment in
+ * CicNotationLexer) *)
+ let initial_symbols =
+ ["\\sub ";"\\sup ";"\\below ";"\\above ";"\\frac "
+ ;"\\infrule ";"\\atop ";"\\over ";"\\root ";"\\of ";"\\sqrt "] in
+ let sym_attributes =
+ Grammar.Entry.create level2_ast_grammar "atag_attributes" in
+ let sym_table =
+ List.fold_left
+ (add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes)
+ [] initial_symbols
+ in
let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
let protected_binder_vars =
Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
- initialize_grammars { level1_pattern=level1_pattern;
+ initialize_grammars loctable
+ { level1_pattern=level1_pattern;
level2_ast=level2_ast;
term=term;
ident=ident;
+ sym_table=sym_table;
+ sym_attributes=sym_attributes;
let_defs=let_defs;
protected_binder_vars=protected_binder_vars;
level2_meta=level2_meta;
class status0 ~keywords:kwds =
object
- val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
+ val db =
+ let lt = ref CicNotationLexer.LocalizeEnv.empty in
+ { grammars = initial_grammars lt kwds; keywords = kwds;
+ items = []; loctable = lt }
method notation_parser_db = db
method set_notation_parser_db v = {< db = v >}
method set_notation_parser_status
: 'status. #g_status as 'status -> 'self
= fun o -> {< db = o#notation_parser_db >}
+ method reset_loctable () =
+ db.loctable := CicNotationLexer.LocalizeEnv.empty
end
-class virtual status ~keywords:kwds =
+class virtual status uid ~keywords:kwds =
object
- inherit NCic.status
+ inherit NCic.status uid
inherit status0 kwds
end
let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
(* move inside constructor XXX *)
let add1item status (level, level1_pattern, action) =
+ let status = update_sym_grammar status level1_pattern in
let p_bindings, p_atoms =
- List.split (extract_term_production status level1_pattern) in
+ List.split (extract_term_production status level1_pattern)
+ in
Grammar.extend
[ Grammar.Entry.obj
(status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
Some (Gramext.Level level),
[ None,
Some (*Gramext.NonA*) Gramext.NonA,
- [ p_atoms,
- (make_action
+ [ p_atoms, (* concrete l1 syntax *)
+ (make_action status
(fun (env: NotationEnv.t) (loc: Ast.location) ->
(action env loc))
p_bindings) ]]];
projects / helm.git / blobdiff