- number notation ported to new library

- code for number notation made less general by hard-coding the only
  notation

diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend
index df0847b170fa04851d9fc45fd22cef9608ca786e..e3e0e7d4412f307541f802f64b87a8b61a53d69b 100644 (file)
--- a/matita/components/ng_disambiguation/.depend
+++ b/matita/components/ng_disambiguation/.depend
@@ -1,13 +1,13 @@
+nnumber_notation.cmi: 
 disambiguateChoices.cmi: 
 nCicDisambiguate.cmi: 
-nnumber_notation.cmi: 
 grafiteDisambiguate.cmi: 
+nnumber_notation.cmo: nnumber_notation.cmi 
+nnumber_notation.cmx: nnumber_notation.cmi 
 disambiguateChoices.cmo: disambiguateChoices.cmi 
 disambiguateChoices.cmx: disambiguateChoices.cmi 
 nCicDisambiguate.cmo: nCicDisambiguate.cmi 
 nCicDisambiguate.cmx: nCicDisambiguate.cmi 
-nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi 
-nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi 
 grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \
     grafiteDisambiguate.cmi 
 grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \

diff --git a/matita/components/ng_disambiguation/Makefile b/matita/components/ng_disambiguation/Makefile
index 8c564325e6e069894d7db3805651981b0e33622b..082d000bc7b1675c5083c69378ab6d53c62d411d 100644 (file)
--- a/matita/components/ng_disambiguation/Makefile
+++ b/matita/components/ng_disambiguation/Makefile
@@ -2,9 +2,9 @@ PACKAGE = ng_disambiguation
 PREDICATES =
 
 INTERFACE_FILES =              \
+       nnumber_notation.mli    \
        disambiguateChoices.mli \
   nCicDisambiguate.mli    \
-       nnumber_notation.mli    \
        grafiteDisambiguate.mli \
        $(NULL)
 IMPLEMENTATION_FILES =         \

diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml
index 3a79d1bfad0403b5d49279832cccd3169d862281..7e3e44f525ccfa8741e457e2301f8896447ffbc1 100644 (file)
--- a/matita/components/ng_disambiguation/disambiguateChoices.ml
+++ b/matita/components/ng_disambiguation/disambiguateChoices.ml
@@ -31,16 +31,13 @@ open DisambiguateTypes
 
 exception Choice_not_found of string Lazy.t
 
-let nnum_choices = ref []
-
-let nadd_num_choice choice = nnum_choices := choice :: !nnum_choices
-
 let has_description dsc = (fun x -> fst x = dsc)
 
 let nlookup_num_by_dsc dsc =
-  try
-    List.find (has_description dsc) !nnum_choices
-  with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^  dsc)))
+ if dsc <> "natural number" then
+  raise (Choice_not_found (lazy ("Num with dsc " ^  dsc)))
+ else
+  "natural number", `Num_interp Nnumber_notation.ninterp_natural_number
 
 let mk_choice  ~mk_appl ~mk_implicit ~term_of_nref (dsc, args, appl_pattern)=
   dsc,

diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli
index 60a938a80b5a5b333d5226dcc58d374b4ec2f858..391fd67ca748bae2741628562260df1447345dd5 100644 (file)
--- a/matita/components/ng_disambiguation/disambiguateChoices.mli
+++ b/matita/components/ng_disambiguation/disambiguateChoices.mli
@@ -30,9 +30,6 @@ open DisambiguateTypes
   (** raised by lookup_XXXX below *)
 exception Choice_not_found of string Lazy.t
 
-  (** register a new number choice *)
-val nadd_num_choice: NCic.term codomain_item -> unit
-
 (** {2 Choices lookup}
  * for user defined aliases *)
 

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index 923ae26125346c4ae63adef3bc68c46ef9297945..490780fbe2e7adadcc2f3b015ec350231a39f994 100644 (file)
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -71,11 +71,6 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases =
  if mode = GrafiteAst.WithoutPreferences then
    status
  else
-   (* MATITA 1.0
-   let new_commands =
-     List.map
-      (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
-   in *)
    let aliases =
     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
      status#disambiguate_db.aliases new_aliases in

diff --git a/matita/components/ng_disambiguation/nnumber_notation.ml b/matita/components/ng_disambiguation/nnumber_notation.ml
index 8eaa705f22995bc3494e14e49f3ce5c3a8df0400..2e5a8fcb5234e251a979b403547adf0804477f84 100644 (file)
--- a/matita/components/ng_disambiguation/nnumber_notation.ml
+++ b/matita/components/ng_disambiguation/nnumber_notation.ml
@@ -41,7 +41,7 @@ let ninterp_natural_number num =
       | None     -> error "no default natural numbers"
    in
   *)
-   let nat_URI = NUri.uri_of_string "cic:/matita/ng/arithmetics/nat/nat.ind" in
+   let nat_URI = NUri.uri_of_string "cic:/matita/arithmetics/nat/nat.ind" in
    let o () =
     NCic.Const
      (NReference.reference_of_spec nat_URI (NReference.Con (0,1,0))) in
@@ -51,8 +51,3 @@ let ninterp_natural_number num =
       (NReference.reference_of_spec nat_URI (NReference.Con (0,2,0)));
       t] in
    build_nat o s num
-
-let _ =
-  DisambiguateChoices.nadd_num_choice
-    ("nnatural number", `Num_interp ninterp_natural_number);
-;;

diff --git a/matita/components/ng_disambiguation/nnumber_notation.mli b/matita/components/ng_disambiguation/nnumber_notation.mli
index 91cba3b7c91490d5f1750c93475590a7063a9e14..dd0a6fbad29d106495f15f7ff99ee25612e89eeb 100644 (file)
--- a/matita/components/ng_disambiguation/nnumber_notation.mli
+++ b/matita/components/ng_disambiguation/nnumber_notation.mli
@@ -25,4 +25,4 @@
 
 (* $Id: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *)
 
-(* Works by side-effects only *)
+val ninterp_natural_number: string -> NCic.term