From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 3 Nov 2010 17:14:35 +0000 (+0000)
Subject: notation kind of works
X-Git-Tag: make_still_working~2740
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=30bbfa78612ca1ad0c131a75d7075cfd35bebbe1;p=helm.git

notation kind of works
---

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<mapsto>>; 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/core_notation.moo b/matita/matita/core_notation.moo
deleted file mode 100644
index 8ba56a73d..000000000
--- a/matita/matita/core_notation.moo
+++ /dev/null
@@ -1,288 +0,0 @@
-(* exists *******************************************************************)
-
-notation "hvbox(∃ _ break . p)"
- with precedence 20
-for @{'exists $p }.
-
-notation < "hvbox(\exists ident i : ty break . p)"
- right associative with precedence 20
-for @{'exists (\lambda ${ident i} : $ty. $p) }.
-
-notation < "hvbox(\exists ident i break . p)"
-  with precedence 20
-for @{'exists (\lambda ${ident i}. $p) }.
-
-(*
-notation < "hvbox(\exists ident i opt (: ty) break . p)"
-  right associative with precedence 20
-for @{ 'exists ${default
-  @{\lambda ${ident i} : $ty. $p}
-  @{\lambda ${ident i} . $p}}}.
-*)
-
-notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
-  with precedence 20
-  for ${ default
-          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
-          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
-       }.
-
-(* sigma ********************************************************************)
-
-notation < "hvbox(\Sigma ident i : ty break . p)"
- left associative with precedence 20
-for @{'sigma (\lambda ${ident i} : $ty. $p) }.
-
-notation < "hvbox(\Sigma ident i break . p)"
- with precedence 20
-for @{'sigma (\lambda ${ident i}. $p) }.
-
-(*
-notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
-  right associative with precedence 20
-for @{ 'sigma ${default
-  @{\lambda ${ident i} : $ty. $p}
-  @{\lambda ${ident i} . $p}}}.
-*)
-
-notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
-  with precedence 20
-  for ${ default
-          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
-          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
-       }.
-
-(* equality, conguence ******************************************************)
-
-notation > "hvbox(a break = b)" 
-  non associative with precedence 45
-for @{ 'eq ? $a $b }.
-
-notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" 
-  non associative with precedence 45
-for @{ 'eq $t $a $b }.
-
-notation > "hvbox(n break (≅ \sub term 90 p) m)"
-  non associative with precedence 45
-for @{ 'congruent $n $m $p }.
-
-notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
-  non associative with precedence 45
-for @{ 'congruent $n $m $p }.
-
-(* other notations **********************************************************)
-
-notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
-with precedence 90 for @{ 'pair $a $b}.
-
-notation "hvbox(x break \times y)" with precedence 70
-for @{ 'product $x $y}.
-
-notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
-notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
-
-notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
-notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
-
-notation > "\fst" with precedence 90 for @{'pi1}.
-notation > "\snd" with precedence 90 for @{'pi2}.
-
-notation "hvbox(a break \to b)" 
-  right associative with precedence 20
-for @{ \forall $_:$a.$b }.
-
-notation < "hvbox(a break \to b)" 
-  right associative with precedence 20
-for @{ \Pi $_:$a.$b }.
-
-notation "hvbox(a break \leq b)" 
-  non associative with precedence 45
-for @{ 'leq $a $b }.
-
-notation "hvbox(a break \geq b)" 
-  non associative with precedence 45
-for @{ 'geq $a $b }.
-
-notation "hvbox(a break \lt b)" 
-  non associative with precedence 45
-for @{ 'lt $a $b }.
-
-notation "hvbox(a break \gt b)" 
-  non associative with precedence 45
-for @{ 'gt $a $b }.
-
-notation > "hvbox(a break \neq b)" 
-  non associative with precedence 45
-for @{ 'neq ? $a $b }.
-
-notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" 
-  non associative with precedence 45
-for @{ 'neq $t $a $b }.
-
-notation "hvbox(a break \nleq b)" 
-  non associative with precedence 45
-for @{ 'nleq $a $b }.
-
-notation "hvbox(a break \ngeq b)" 
-  non associative with precedence 45
-for @{ 'ngeq $a $b }.
-
-notation "hvbox(a break \nless b)" 
-  non associative with precedence 45
-for @{ 'nless $a $b }.
-
-notation "hvbox(a break \ngtr b)" 
-  non associative with precedence 45
-for @{ 'ngtr $a $b }.
-
-notation "hvbox(a break \divides b)"
-  non associative with precedence 45
-for @{ 'divides $a $b }.
-
-notation "hvbox(a break \ndivides b)"
-  non associative with precedence 45
-for @{ 'ndivides $a $b }.
-
-notation "hvbox(a break + b)" 
-  left associative with precedence 50
-for @{ 'plus $a $b }.
-
-notation "hvbox(a break - b)" 
-  left associative with precedence 50
-for @{ 'minus $a $b }.
-
-notation "hvbox(a break * b)" 
-  left associative with precedence 55
-for @{ 'times $a $b }.
-
-notation "hvbox(a break \middot b)" 
-  left associative with precedence 55
-  for @{ 'middot $a $b }.
-
-notation "hvbox(a break \mod b)" 
-  left associative with precedence 55
-for @{ 'module $a $b }.
-
-notation < "a \frac b" 
-  non associative with precedence 90
-for @{ 'divide $a $b }.
-
-notation "a \over b" 
-  left associative with precedence 55
-for @{ 'divide $a $b }.
-
-notation "hvbox(a break / b)" 
-  left associative with precedence 55
-for @{ 'divide $a $b }.
-
-notation "- term 60 a" with precedence 60 
-for @{ 'uminus $a }.
-
-notation "a !"
-  non associative with precedence 80
-for @{ 'fact $a }.
-
-notation "\sqrt a" 
-  non associative with precedence 60
-for @{ 'sqrt $a }.
-
-notation "hvbox(a break \lor b)" 
-  left associative with precedence 30
-for @{ 'or $a $b }.
-
-notation "hvbox(a break \land b)" 
-  left associative with precedence 35
-for @{ 'and $a $b }.
-
-notation "hvbox(\lnot a)" 
-  non associative with precedence 40
-for @{ 'not $a }.
-
-notation > "hvbox(a break \liff b)" 
-  left associative with precedence 25
-for @{ 'iff $a $b }.
-
-notation "hvbox(a break \leftrightarrow b)" 
-  left associative with precedence 25
-for @{ 'iff $a $b }.
-
-
-notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
-for @{ 'powerset $A }.
-notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
-for @{ 'powerset $A }.
-
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
-
-notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }. (* \between *)
-
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
-
-notation "hvbox(a break ∩ b)" left associative with precedence 55
-for @{ 'intersects $a $b }. (* \cap *)
-
-notation "hvbox(a break ∪ b)" left associative with precedence 50
-for @{ 'union $a $b }. (* \cup *)
-
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
-
-notation "hvbox(a break \approx b)" non associative with precedence 45 
-  for @{ 'napart $a $b}.
-        
-notation "hvbox(a break # b)" non associative with precedence 45 
-  for @{ 'apart $a $b}.
-    
-notation "hvbox(a break \circ b)" 
-  left associative with precedence 55
-for @{ 'compose $a $b }.
-
-notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
-notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
-
-notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
-
-notation "↑a" with precedence 55 for @{ 'uparrow $a }.
-
-notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
-
-notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
-notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
-notation > "a ^ term 90 b"  non associative with precedence 75 for @{ 'exp $a $b}.
-notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
-notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
-notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. 
-
-notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
-
-notation "\naturals" non associative with precedence 90 for @{'N}.
-notation "\rationals" non associative with precedence 90 for @{'Q}.
-notation "\reals" non associative with precedence 90 for @{'R}.
-notation "\integers" non associative with precedence 90 for @{'Z}.
-notation "\complexes" non associative with precedence 90 for @{'C}.
-
-notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
-
-notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
-notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation > "⊩ " with precedence 60 for @{'Vdash ?}.
-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}.
-
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/nlibrary/core_notation.ma b/matita/matita/nlibrary/core_notation.ma
new file mode 100644
index 000000000..9cc0cca3c
--- /dev/null
+++ b/matita/matita/nlibrary/core_notation.ma
@@ -0,0 +1,287 @@
+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+  with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'exists ${default
+  @{\lambda ${ident i} : $ty. $p}
+  @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+  with precedence 20
+  for ${ default
+          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+       }.
+
+(* sigma ********************************************************************)
+
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'sigma ${default
+  @{\lambda ${ident i} : $ty. $p}
+  @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
+  with precedence 20
+  for ${ default
+          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
+          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
+       }.
+
+(* equality, conguence ******************************************************)
+
+notation > "hvbox(a break = b)" 
+  non associative with precedence 45
+for @{ 'eq ? $a $b }.
+
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" 
+  non associative with precedence 45
+for @{ 'eq $t $a $b }.
+
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
+  non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
+  non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+(* other notations **********************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
+
+notation "hvbox(a break \to b)" 
+  right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(a break \to b)" 
+  right associative with precedence 20
+for @{ \Pi $_:$a.$b }.
+
+notation "hvbox(a break \leq b)" 
+  non associative with precedence 45
+for @{ 'leq $a $b }.
+
+notation "hvbox(a break \geq b)" 
+  non associative with precedence 45
+for @{ 'geq $a $b }.
+
+notation "hvbox(a break \lt b)" 
+  non associative with precedence 45
+for @{ 'lt $a $b }.
+
+notation "hvbox(a break \gt b)" 
+  non associative with precedence 45
+for @{ 'gt $a $b }.
+
+notation > "hvbox(a break \neq b)" 
+  non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" 
+  non associative with precedence 45
+for @{ 'neq $t $a $b }.
+
+notation "hvbox(a break \nleq b)" 
+  non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)" 
+  non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)" 
+  non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)" 
+  non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
+notation "hvbox(a break \divides b)"
+  non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+  non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
+notation "hvbox(a break + b)" 
+  left associative with precedence 50
+for @{ 'plus $a $b }.
+
+notation "hvbox(a break - b)" 
+  left associative with precedence 50
+for @{ 'minus $a $b }.
+
+notation "hvbox(a break * b)" 
+  left associative with precedence 55
+for @{ 'times $a $b }.
+
+notation "hvbox(a break \middot b)" 
+  left associative with precedence 55
+  for @{ 'middot $a $b }.
+
+notation "hvbox(a break \mod b)" 
+  left associative with precedence 55
+for @{ 'module $a $b }.
+
+notation < "a \frac b" 
+  non associative with precedence 90
+for @{ 'divide $a $b }.
+
+notation "a \over b" 
+  left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "hvbox(a break / b)" 
+  left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "- term 60 a" with precedence 60 
+for @{ 'uminus $a }.
+
+notation "a !"
+  non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "\sqrt a" 
+  non associative with precedence 60
+for @{ 'sqrt $a }.
+
+notation "hvbox(a break \lor b)" 
+  left associative with precedence 30
+for @{ 'or $a $b }.
+
+notation "hvbox(a break \land b)" 
+  left associative with precedence 35
+for @{ 'and $a $b }.
+
+notation "hvbox(\lnot a)" 
+  non associative with precedence 40
+for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" left associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" left associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45 
+  for @{ 'napart $a $b}.
+        
+notation "hvbox(a break # b)" non associative with precedence 45 
+  for @{ 'apart $a $b}.
+    
+notation "hvbox(a break \circ b)" 
+  left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
+notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+
+notation "↑a" with precedence 55 for @{ 'uparrow $a }.
+
+notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
+
+notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a ^ term 90 b"  non associative with precedence 75 for @{ 'exp $a $b}.
+notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. 
+
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+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}.