From ba2dfe6409e95bf9e558dc0d4be382b068671409 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 13 Jul 2005 09:44:01 +0000 Subject: [PATCH] snapshot - added keyword handling for notation specifying string literals - added keywords to level2_ast_lexer --- helm/ocaml/cic_notation/cicNotationLexer.ml | 53 +++++++--- helm/ocaml/cic_notation/cicNotationLexer.mli | 3 + helm/ocaml/cic_notation/cicNotationParser.ml | 102 +++++++++++-------- helm/ocaml/cic_notation/cicNotationPp.ml | 10 +- helm/ocaml/cic_notation/cicNotationPres.ml | 5 +- helm/ocaml/cic_notation/cicNotationPres.mli | 3 +- helm/ocaml/cic_notation/cicNotationPt.ml | 1 + helm/ocaml/cic_notation/cicNotationRew.ml | 3 +- helm/ocaml/cic_notation/cicNotationRew.mli | 2 + helm/ocaml/cic_notation/cicNotationUtil.ml | 28 +++-- helm/ocaml/cic_notation/cicNotationUtil.mli | 3 + helm/ocaml/cic_notation/doc/samples.ma | 7 +- helm/ocaml/cic_notation/test_parser.ml | 24 +++-- 13 files changed, 154 insertions(+), 90 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 26dc5aaca..01ef6142c 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -62,6 +62,14 @@ let level1_layouts = "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"; @@ -70,13 +78,19 @@ let level2_meta_keywords = "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 *) @@ -173,26 +187,38 @@ let rec level2_meta_token = lexer 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", "") @@ -209,7 +235,8 @@ let rec level1_pattern_token = lexer 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", "") diff --git a/helm/ocaml/cic_notation/cicNotationLexer.mli b/helm/ocaml/cic_notation/cicNotationLexer.mli index 33ba97e2b..5eb22a99c 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.mli +++ b/helm/ocaml/cic_notation/cicNotationLexer.mli @@ -32,3 +32,6 @@ val level1_pattern_lexer: (string * string) Token.glexer 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 *) + diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index b64fdb5ee..01ed2906b 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} *) @@ -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 ] ]; (* }}} *) diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index f8b8acba0..e04b00b70 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -36,12 +36,10 @@ let pp_binder = function | `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 -> diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 83bb10878..c3ea73f1c 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -31,6 +31,7 @@ type markup = mathml_markup 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" *) @@ -214,8 +215,8 @@ let render ids_to_uris = 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 diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli index d7fcb9ea3..68da94458 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.mli +++ b/helm/ocaml/cic_notation/cicNotationPres.mli @@ -28,7 +28,8 @@ and boxml_markup = mathml_markup Box.box 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: diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 9c5257e07..99b8909e5 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -147,4 +147,5 @@ type phrase = (* TODO hackish: replace with TacticAst.statement or similar *) (* level 1 pattern, associativity, precedence, level 2 pattern *) | Interpretation of (string * argument_pattern list) * cic_appl_pattern | Render of UriManager.uri + | Dump (* dump grammar *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index f3f6cac2a..207b26a23 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -323,7 +323,8 @@ let instantiate21 env (* precedence associativity *) l1 = 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 diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 21877d0c3..cb43b3099 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -33,6 +33,8 @@ val ast_of_acic: (** 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 diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 24b4af1d9..1f9d9f5cc 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -100,7 +100,6 @@ let fresh_name = 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) @@ -117,13 +116,11 @@ let visit_ast ?(special_k = fun _ -> assert false) k = | 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 _ @@ -131,24 +128,16 @@ let visit_ast ?(special_k = fun _ -> assert false) k = | 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 @@ -207,6 +196,23 @@ let names_of_term t = 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 diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index a03c415d2..fd7e12f7f 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -28,6 +28,9 @@ val fresh_name: unit -> string 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) -> diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index f1f6ac939..46193bf73 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -51,8 +51,7 @@ notation "'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" @@ -61,9 +60,9 @@ for 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 diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 522baaccc..1673db6f4 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,9 +25,7 @@ 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) = @@ -52,6 +50,7 @@ let _ = 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 "===="; @@ -63,16 +62,16 @@ let _ = | 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); @@ -85,6 +84,7 @@ let _ = 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, _, _, _ = @@ -111,13 +111,17 @@ let _ = 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%s%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 -> () -- 2.39.2