From 30bbfa78612ca1ad0c131a75d7075cfd35bebbe1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 Nov 2010 17:14:35 +0000 Subject: [PATCH] notation kind of works --- .../content_pres/cicNotationParser.ml | 93 +++++++++---------- .../content_pres/cicNotationParser.mli | 2 +- .../grafite_engine/grafiteEngine.ml | 11 ++- matita/components/grafite_parser/.depend | 3 - matita/components/grafite_parser/.depend.opt | 10 +- matita/components/grafite_parser/Makefile | 1 - .../components/grafite_parser/cicNotation2.ml | 40 -------- .../grafite_parser/cicNotation2.mli | 29 ------ .../grafite_parser/grafiteParser.ml | 33 ++++--- .../grafite_parser/grafiteParser.mli | 5 + matita/components/lexicon/lexiconTypes.ml | 2 +- matita/matita/matitaScript.ml | 5 +- matita/matita/matitacLib.ml | 5 +- .../core_notation.ma} | 1 - 14 files changed, 79 insertions(+), 161 deletions(-) delete mode 100644 matita/components/grafite_parser/cicNotation2.ml delete mode 100644 matita/components/grafite_parser/cicNotation2.mli rename matita/matita/{core_notation.moo => nlibrary/core_notation.ma} (99%) diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index b828f8bc5..c22953314 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -48,6 +48,11 @@ type ('a,'b,'c,'d) grammars = { type checked_l1_pattern = CL1P of NotationPt.term * int +type binding = + | NoBinding + | Binding of string * Env.value_type + | Env of (string * Env.value_type) list + type db = { grammars: (int -> NotationPt.term, @@ -55,7 +60,8 @@ type db = { (Ast.term Ast.capture_variable list * Ast.term Ast.capture_variable * Ast.term * int) list, Ast.term list * Ast.term option) grammars; - items: (checked_l1_pattern * int * Gramext.g_assoc * NotationPt.term) list + keywords: string list; + items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list } let int_of_string s = @@ -80,7 +86,7 @@ let gram_term status = function | Ast.Level precedence -> Gramext.Snterml (Grammar.Entry.obj - (status#notation_parser_db.grammars.term: 'a Grammar.Entry.e), + (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e), level_of precedence) ;; @@ -90,11 +96,6 @@ let gram_of_literal = | `Keyword s -> gram_keyword s | `Number s -> gram_number s -type binding = - | NoBinding - | Binding of string * Env.value_type - | Env of (string * Env.value_type) list - let make_action action bindings = let rec aux (vl : NotationEnv.t) = function @@ -316,43 +317,6 @@ let check_l1_pattern level1_pattern pponly level associativity = CL1P (cp,level) ;; -let extend status (CL1P (level1_pattern,precedence)) action = - assert false -(* - CicNotationParser.new_parser (); - let create_cb_old (l1, precedence, associativity, l2) = - ignore( - CicNotationParser.extend l1 - (fun env loc -> - NotationPt.AttributedTerm - (`Loc loc,TermContentPres.instantiate_level2 env l2))) - in - RefCounter.iter create_cb_old !parser_ref_counter; -*) -(* - let p_bindings, p_atoms = - List.split (extract_term_production status level1_pattern) - in - let level = level_of precedence in - let () = - 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 - (fun (env: NotationEnv.t) (loc: Ast.location) -> - (action env loc)) - p_bindings) ]]] - in - let keywords = NotationUtil.keywords_of_term level1_pattern in - let rule_id = p_atoms in - List.iter CicNotationLexer.add_level2_ast_keyword keywords; - rule_id -*) - (** {2 Grammar} *) let fold_cluster binder terms ty body = @@ -797,8 +761,8 @@ END grammars ;; -let initial_grammars = - let lexers = CicNotationLexer.mk_lexers [] in +let initial_grammars keywords = + let lexers = CicNotationLexer.mk_lexers keywords in let level1_pattern_grammar = Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in let level2_ast_grammar = @@ -828,9 +792,9 @@ class type g_status = method notation_parser_db: db end -class status = - object(self) - val db = { grammars = initial_grammars ; items = [] } +class status ~keywords:kwds = + object + val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] } method notation_parser_db = db method set_notation_parser_db v = {< db = v >} method set_notation_parser_status @@ -838,6 +802,37 @@ class status = = fun o -> {< db = o#notation_parser_db >} end +let extend (status : #status) (CL1P (level1_pattern,precedence)) action = + (* move inside constructor XXX *) + let add1item status (level, level1_pattern, action) = + let p_bindings, p_atoms = + 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 + (fun (env: NotationEnv.t) (loc: Ast.location) -> + (action env loc)) + p_bindings) ]]]; + status + in + let current_item = + let level = level_of precedence in + level, level1_pattern, action in + let keywords = NotationUtil.keywords_of_term level1_pattern @ + status#notation_parser_db.keywords in + let items = current_item :: status#notation_parser_db.items in + let status = status#set_notation_parser_status (new status ~keywords) in + let status = status#set_notation_parser_db + {status#notation_parser_db with items = items} in + List.fold_left add1item status items +;; + + let parse_level1_pattern status = parse_level1_pattern status#notation_parser_db.grammars let parse_level2_ast status = diff --git a/matita/components/content_pres/cicNotationParser.mli b/matita/components/content_pres/cicNotationParser.mli index b70eb141f..62262c14c 100644 --- a/matita/components/content_pres/cicNotationParser.mli +++ b/matita/components/content_pres/cicNotationParser.mli @@ -33,7 +33,7 @@ class type g_status = method notation_parser_db: db end -class status: +class status: keywords:string list -> object('self) inherit g_status method set_notation_parser_db: db -> 'self diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index e96790860..a70e78855 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -589,12 +589,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern in - let mode = assert false in (* VEDI SOTTO *) + let mode = GrafiteAst.WithPreferences (*assert false*) in (* VEDI SOTTO *) let diff = [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)] in let status = LexiconEngine.set_proof_aliases status mode diff in - assert false (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO + status, [] + (*assert false*) (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO IL MODE WithPreference/WithOutPreferences*) | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> let l1 = @@ -603,7 +604,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = in let status = if dir <> Some `RightToLeft then - CicNotationParser.extend status l1 + GrafiteParser.extend status l1 (fun env loc -> NotationPt.AttributedTerm (`Loc loc,TermContentPres.instantiate_level2 env l2)) @@ -616,8 +617,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = else status in - assert false (* MANCA SALVATAGGIO SU DISCO *) - status +(* assert false (* MANCA SALVATAGGIO SU DISCO *) *) + status, [] (* capire [] XX *) | GrafiteAst.Alias (loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding diff --git a/matita/components/grafite_parser/.depend b/matita/components/grafite_parser/.depend index dff050549..e45f9bef8 100644 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@ -1,14 +1,11 @@ dependenciesParser.cmi: grafiteParser.cmi: -cicNotation2.cmi: grafiteDisambiguate.cmi: print_grammar.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi -cicNotation2.cmo: cicNotation2.cmi -cicNotation2.cmx: cicNotation2.cmi grafiteDisambiguate.cmo: grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguate.cmi print_grammar.cmo: print_grammar.cmi diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index 2766b04d0..e45f9bef8 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,17 +1,11 @@ dependenciesParser.cmi: grafiteParser.cmi: -cicNotation2.cmi: -nEstatus.cmi: -grafiteDisambiguate.cmi: nEstatus.cmi -print_grammar.cmi: +grafiteDisambiguate.cmi: +print_grammar.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi -cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi -cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi -nEstatus.cmo: nEstatus.cmi -nEstatus.cmx: nEstatus.cmi grafiteDisambiguate.cmo: grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguate.cmi print_grammar.cmo: print_grammar.cmi diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index c1288b4ab..631e40eb4 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -4,7 +4,6 @@ PREDICATES = INTERFACE_FILES = \ dependenciesParser.mli \ grafiteParser.mli \ - cicNotation2.mli \ grafiteDisambiguate.mli \ print_grammar.mli \ $(NULL) diff --git a/matita/components/grafite_parser/cicNotation2.ml b/matita/components/grafite_parser/cicNotation2.ml deleted file mode 100644 index 47a21ae62..000000000 --- a/matita/components/grafite_parser/cicNotation2.ml +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let load_notation status ~include_paths fname = - assert false -(* - let ic = open_in fname in - let lexbuf = Ulexing.from_utf8_channel ic in - let status = ref status in - try - while true do - status := fst (GrafiteParser.parse_statement lexbuf !status) - done; - assert false - with End_of_file -> close_in ic; !status -*) diff --git a/matita/components/grafite_parser/cicNotation2.mli b/matita/components/grafite_parser/cicNotation2.mli deleted file mode 100644 index d6cdfe852..000000000 --- a/matita/components/grafite_parser/cicNotation2.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(** @param fname file from which load notation *) -val load_notation: - #LexiconTypes.status as 'status -> include_paths:string list -> string -> - 'status diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index b3e42e63e..948519086 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -578,6 +578,7 @@ EXTEND m = LIST0 [ u1 = URI; SYMBOL <:unicode>; u2 = URI -> u1,u2 ] -> G.NCopy (loc,s,NUri.uri_of_string u, List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m) + | lc = lexicon_command -> lc ]]; lexicon_command: [ [ @@ -617,12 +618,6 @@ EXTEND LSome (G.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> LSome (G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname)))) - | scom = lexicon_command ; SYMBOL "." -> - assert false -(* - let status = LE.eval_command status scom in - status, LNone loc -*) | EOI -> raise End_of_file ] ]; @@ -640,19 +635,27 @@ class type g_status = end class status = - let lstatus = assert false in - let grammar = CicNotationParser.level2_ast_grammar lstatus in - object - inherit LexiconTypes.status - val db = - mk_parser (Grammar.Entry.create grammar "statement") lstatus - method parser_db = db - method set_parser_db v = {< db = v >} + object(self) + inherit LexiconTypes.status as super + val mutable db = None + method parser_db = match db with None -> assert false | Some x -> x + method set_parser_db v = {< db = Some v >} method set_parser_status : 'status. #g_status as 'status -> 'self - = fun o -> {< db = o#parser_db >}#set_lexicon_engine_status o + = fun o -> {< db = Some o#parser_db >}#set_lexicon_engine_status o + initializer + let grammar = CicNotationParser.level2_ast_grammar self in + db <- Some (mk_parser (Grammar.Entry.create grammar "statement") self) end +let extend status l1 action = + let status = CicNotationParser.extend status l1 action in + let grammar = CicNotationParser.level2_ast_grammar status in + status#set_parser_db + (mk_parser (Grammar.Entry.create grammar "statement") status) +;; + + let parse_statement status = parse_statement status#parser_db diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli index dc39ab316..11fbccaed 100644 --- a/matita/components/grafite_parser/grafiteParser.mli +++ b/matita/components/grafite_parser/grafiteParser.mli @@ -45,6 +45,11 @@ class status : method set_parser_status : 'status. #g_status as 'status -> 'self end +val extend : #status as 'status -> + CicNotationParser.checked_l1_pattern -> + (NotationEnv.t -> NotationPt.location -> NotationPt.term) -> 'status + + (* never_include: do not call LexiconEngine to do includes, * always raise NoInclusionPerformed *) (** @raise End_of_file *) diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml index f0cf75946..5e6a0a326 100644 --- a/matita/components/lexicon/lexiconTypes.ml +++ b/matita/components/lexicon/lexiconTypes.ml @@ -47,7 +47,7 @@ class status = object(self) inherit Interpretations.status inherit TermContentPres.status - inherit CicNotationParser.status + inherit CicNotationParser.status ~keywords:[] val lstatus = initial_status method lstatus = lstatus method set_lstatus v = {< lstatus = v >} diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 864583d88..b8a72a4d2 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -284,10 +284,7 @@ let initial_statuses current baseuri = (* CSC: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () | None -> ()); - let lexicon_status = - CicNotation2.load_notation ~include_paths:[] empty_lstatus - BuildTimeConf.core_notation_script - in + let lexicon_status = empty_lstatus in let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in grafite_status in diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 23a0ca15f..cf037531f 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -122,10 +122,7 @@ let compile atstart options fname = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; activate_extraction baseuri fname ; - let lexicon_status = - CicNotation2.load_notation ~include_paths:[] (new LexiconTypes.status) - BuildTimeConf.core_notation_script - in + let lexicon_status = new LexiconTypes.status in atstart (); (* FG: do not invoke before loading the core notation script *) let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in diff --git a/matita/matita/core_notation.moo b/matita/matita/nlibrary/core_notation.ma similarity index 99% rename from matita/matita/core_notation.moo rename to matita/matita/nlibrary/core_notation.ma index 8ba56a73d..9cc0cca3c 100644 --- a/matita/matita/core_notation.moo +++ b/matita/matita/nlibrary/core_notation.ma @@ -285,4 +285,3 @@ notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. notation < "maction (mstyle color #ff0000 (­…­)) (t)" non associative with precedence 90 for @{'hide $t}. - -- 2.39.2