"sqrt"; "root"
]
+let level1_keywords =
+ [ "hbox"; "hvbox"; "hovbox"; "vbox";
+ "break";
+ "list0"; "list1"; "sep";
+ "opt";
+ "term"; "ident"; "number"
+ ] @ level1_layouts
+
let level2_meta_keywords =
[ "if"; "then"; "else";
"fold"; "left"; "right"; "rec";
"anonymous"; "ident"; "number"; "term"; "fresh"
]
-let level1_keywords =
- [ "hbox"; "hvbox"; "hovbox"; "vbox";
- "break";
- "list0"; "list1"; "sep";
- "opt";
- "term"; "ident"; "number"
- ]
+ (* (string, unit) Hashtbl.t, to exploit multiple bindings *)
+let level2_ast_keywords = Hashtbl.create 23
+let _ =
+ (* TODO ZACK: keyword list almost cut and paste from cicTextualLexer2.ml, to
+ * be reviewed *)
+ List.iter (fun k -> Hashtbl.add level2_ast_keywords k ())
+ [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; "with"; "in";
+ "and"; "on" ]
+
+let add_level2_ast_keyword k =
+ prerr_endline ("Adding keyword " ^ k);
+ Hashtbl.add level2_ast_keywords k ()
+let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k
let regexp uri =
("cic:/" | "theory:/") (* schema *)
return lexbuf ("IDENT", s)
end
| "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
- | ast_ident -> return lexbuf ("UNPARSED_AST", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
- | ast_csymbol -> return lexbuf ("UNPARSED_AST", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | ast_ident ->
+ return lexbuf ("UNPARSED_AST",
+ remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | ast_csymbol ->
+ return lexbuf ("UNPARSED_AST",
+ remove_left_quote (Ulexing.utf8_lexeme lexbuf))
| eof -> return lexbuf ("EOI", "")
let rec level2_ast_token = lexer
| xml_blank+ -> level2_ast_token lexbuf
| meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
| implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
- | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
+ | ident ->
+ let lexeme = Ulexing.utf8_lexeme lexbuf in
+ if Hashtbl.mem level2_ast_keywords lexeme then
+ return lexbuf ("", lexeme)
+ else
+ return lexbuf ("IDENT", lexeme)
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
| keyword -> return lexbuf (keyword lexbuf)
| tex_token -> return lexbuf (expand_macro lexbuf)
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
- | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
+ | qstring ->
+ return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
| csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
| "${" -> read_unparsed_group "UNPARSED_META" lexbuf
| "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
| '(' -> return lexbuf ("LPAREN", "")
| ')' -> return lexbuf ("RPAREN", "")
- | meta_ident -> return lexbuf ("UNPARSED_META", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | meta_ident ->
+ return lexbuf ("UNPARSED_META",
+ remove_left_quote (Ulexing.utf8_lexeme lexbuf))
| meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
| _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
| eof -> return lexbuf ("EOI", "")
return lexbuf ("IDENT", s)
end
| tex_token -> return lexbuf (expand_macro lexbuf)
- | qkeyword -> return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
+ | qkeyword ->
+ return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
| '(' -> return lexbuf ("LPAREN", "")
| ')' -> return lexbuf ("RPAREN", "")
| eof -> return lexbuf ("EOI", "")
val level2_ast_lexer: (string * string) Token.glexer
val level2_meta_lexer: (string * string) Token.glexer
+val add_level2_ast_keyword: string -> unit (** non idempotent *)
+val remove_level2_ast_keyword: string -> unit (** non idempotent *)
+
(** {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
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 =
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 =
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
=
(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} *)
(* {{{ 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: [
]
];
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<def>> (* ≝ *); body = term ->
let body = fold_binder `Lambda args body in
| 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<def>> (* ≝ *);
+ [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
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))
]
| 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<Rightarrow>> (* ⇒ *);
rhs = term ->
]
];
precedence: [
- [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
+ [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
];
notation: [
[ s = QSTRING;
| 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
]
];
(* }}} *)
| `Exists -> "exists"
| `Forall -> "forall"
-let pp_literal l =
- sprintf "literal(%s)"
- (match l with
- | `Symbol s
- | `Keyword s
- | `Number s -> s)
+let pp_literal = function
+ | `Symbol s -> sprintf "symbol(%s)" s
+ | `Keyword s -> sprintf "keyword(%s)" s
+ | `Number s -> sprintf "number(%s)" s
let rec pp_term = function
| AttributedTerm (`Href _, term) when print_attributes ->
let atop_attributes = [None, "linethickness", "0pt"]
let binder_attributes = [None, "mathcolor", "blue"]
let indent_attributes = [None, "indent", "1em"]
+let keyword_attributes = [None, "mathcolor", "blue"]
let mpres_arrow = Mpresentation.Mo (binder_attributes, "->")
(* TODO unicode symbol "to" *)
and aux_literal xref prec uris l =
let attrs = make_href xref uris in
match l with
- | `Symbol s
- | `Keyword s -> P.Mo (attrs, to_unicode s)
+ | `Symbol s -> P.Mo (attrs, to_unicode s)
+ | `Keyword s -> P.Mo (keyword_attributes @ attrs, to_unicode s)
| `Number s -> P.Mn (attrs, to_unicode s)
and aux_layout mathonly xref pos prec uris l =
let attrs = make_xref xref in
type markup = mathml_markup
-(** @param ids_to_uris mapping id -> uri for hyperlinking *)
+(** level 1 -> level 0
+ * @param ids_to_uris mapping id -> uri for hyperlinking *)
val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup
val render_to_boxml:
(* level 1 pattern, associativity, precedence, level 2 pattern *)
| Interpretation of (string * argument_pattern list) * cic_appl_pattern
| Render of UriManager.uri
+ | Dump (* dump grammar *)
end
| _ -> assert false (* impossible *)
and subst_layout env = function
- | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+ | Ast.Box (kind, tl) ->
+ Ast.Box (kind, List.concat (List.map (subst env) tl))
| l -> CicNotationUtil.visit_layout (subst_singleton env) l
in
subst_singleton env l1
(** level 2 -> level 1 *)
val pp_ast: CicNotationPt.term -> CicNotationPt.term
+(** level 1 -> level 0: see CicNotationPres.render *)
+
type interpretation_id
type pretty_printer_id
let visit_ast ?(special_k = fun _ -> assert false) k =
let rec aux = function
-
| Appl terms -> Appl (List.map k terms)
| Binder (kind, var, body) ->
Binder (kind, aux_capture_variable var, k body)
| Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
| Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
| Meta (index, substs) -> Meta (index, List.map aux_opt substs)
-
| (AttributedTerm _
| Layout _
| Literal _
| Magic _
| Variable _) as t -> special_k t
-
| (Ident _
| Implicit
| Num _
| Symbol _
| Uri _
| UserInput) as t -> t
-
and aux_opt = function
| None -> None
| Some term -> Some (k term)
-
and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
-
and aux_patterns patterns = List.map aux_pattern patterns
-
and aux_pattern ((head, vars), term) =
((head, List.map aux_capture_variable vars), k term)
-
and aux_subst (name, term) = (name, k term)
-
and aux_substs substs = List.map aux_subst substs
-
in
-
aux
let visit_layout k = function
in
List.map aux (variables_of_term t)
+let keywords_of_term t =
+ let rec keywords = ref [] in
+ let add_keyword k = keywords := k :: !keywords in
+ let rec aux = function
+ | AttributedTerm (_, t) -> aux t
+ | Layout l -> Layout (visit_layout aux l)
+ | Literal (`Keyword k) as t ->
+ add_keyword k;
+ t
+ | Literal _ as t -> t
+ | Magic m -> Magic (visit_magic aux m)
+ | Variable _ as v -> v
+ | t -> visit_ast aux t
+ in
+ ignore (aux t) ;
+ !keywords
+
let rec strip_attributes t =
let special_k = function
| AttributedTerm (_, term) -> strip_attributes term
val variables_of_term: CicNotationPt.term -> CicNotationPt.pattern_variable list
val names_of_term: CicNotationPt.term -> string list
+ (** extract all keywords (i.e. string literals) from a level 1 pattern *)
+val keywords_of_term: CicNotationPt.term -> string list
+
val visit_ast:
?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
(CicNotationPt.term -> CicNotationPt.term) ->
"'if' a 'then' b 'else' c"
for
@{ 'ifthenelse $a $b $c }.
-
-TODO collezionare le keyword e aggiungerle al lexer nonche' ricordarsele per quando si rimuove la notazione.
+print if even then x else bump x.
notation
"a \vee b"
notation
"'fun' ident x \to a"
- right associative at precedence ...
+ right associative with precedence 20
for
- @{ 'lambda ${ident x} $a }
+ @{ 'lambda ${ident x} $a }.
NOTES
open Printf
-let _ =
- Helm_registry.load_from "test_parser.conf.xml"
-(* Http_getter.init () *)
+let _ = Helm_registry.load_from "test_parser.conf.xml"
let xml_stream_of_markup =
let rec print_box (t: CicNotationPres.boxml_markup) =
try
let istream = Stream.of_channel stdin in
while Stream.peek istream <> None do
+ try
match CicNotationParser.parse_phrase istream with
| P.Print t ->
prerr_endline "====";
| P.Notation (l1, associativity, precedence, l2) ->
prerr_endline "Extending parser ..."; flush stdout;
prerr_endline (CicNotationPp.pp_term l1) ;
+ prerr_endline (sprintf "Found keywords: %s"
+ (String.concat " " (CicNotationUtil.keywords_of_term l1)));
let time1 = Unix.gettimeofday () in
- ignore
- (CicNotationParser.extend l1 ?precedence ?associativity
- (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
+ ignore (CicNotationParser.extend l1 ?precedence ?associativity
+ (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
let time2 = Unix.gettimeofday () in
prerr_endline "Extending pretty printer ..."; flush stdout;
let time3 = Unix.gettimeofday () in
- ignore
- (CicNotationRew.add_pretty_printer ?precedence ?associativity
- l2 l1);
+ ignore (CicNotationRew.add_pretty_printer
+ ?precedence ?associativity l2 l1);
let time4 = Unix.gettimeofday () in
printf "done (extending parser took %f, extending pretty printer took %f)\n"
(time2 -. time1) (time4 -. time3);
printf "done (patterns compilation took %f seconds)\n"
(time2 -. time1);
flush stdout
+ | P.Dump -> CicNotationParser.print_l2_pattern (); print_newline ()
| P.Render uri ->
let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
let annobj, _, _, id_to_sort, _, _, _ =
prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3));
prerr_endline (CicNotationPp.pp_term t');
dump_xml t' id_to_uri "out.xml"
-(* CicNotationParser.print_l2_pattern () *)
(* let (x, y) = P.loc_of_floc floc in *)
(* let before = String.sub line 0 x in *)
(* let error = String.sub line x (y - x) in *)
(* let after = String.sub line y (String.length line - y) in *)
(* eprintf "%s\e[01;31m%s\e[00m%s\n" before error after; *)
(* prerr_endline (sprintf "at character %d-%d: %s" x y msg) *)
+ with
+ | End_of_file -> raise End_of_file
+ | exn ->
+ prerr_endline
+ (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
done
with End_of_file ->
()
projects / helm.git / commitdiff