From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Nov 2010 10:44:56 +0000 (+0000)
Subject: - number notation ported to new library
X-Git-Tag: make_still_working~2695
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4556677f40e6b979d9bdaa4475bb1ca6701264f8;p=helm.git

- 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 df0847b17..e3e0e7d44 100644
--- 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 8c564325e..082d000bc 100644
--- 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 3a79d1bfa..7e3e44f52 100644
--- 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 60a938a80..391fd67ca 100644
--- 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 923ae2612..490780fbe 100644
--- 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 8eaa705f2..2e5a8fcb5 100644
--- 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 91cba3b7c..dd0a6fbad 100644
--- 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