Number notation for NG.

diff --git a/helm/software/components/METAS/meta.helm-ng_disambiguation.src b/helm/software/components/METAS/meta.helm-ng_disambiguation.src
index 59c5f5ec5a30b0c9eca9f4d7da6dace94a20ecda..7693d8f3cb87a490e72b4a35c01644c781eccdc8 100644 (file)
--- a/helm/software/components/METAS/meta.helm-ng_disambiguation.src
+++ b/helm/software/components/METAS/meta.helm-ng_disambiguation.src
@@ -1,4 +1,4 @@
-requires="helm-whelp helm-acic_content helm-ng_refiner helm-disambiguation"
+requires="helm-whelp helm-acic_content helm-ng_refiner helm-disambiguation helm-cic_disambiguation"
 version="0.0.1"
 archive(byte)="ng_disambiguation.cma"
 archive(native)="ng_disambiguation.cmxa"

diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
index f0c7b373ff9da2f8b1082f7a163dfed780c4e453..6d4d63b704e367c0c64cf3f0989d8c68de527031 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
@@ -32,8 +32,10 @@ open DisambiguateTypes
 exception Choice_not_found of string Lazy.t
 
 let num_choices = ref []
+let nnum_choices = ref []
 
 let add_num_choice choice = num_choices := choice :: !num_choices
+let nadd_num_choice choice = nnum_choices := choice :: !nnum_choices
 
 let has_description dsc = (fun x -> fst x = dsc)
 
@@ -44,6 +46,11 @@ let lookup_num_by_dsc dsc =
     List.find (has_description dsc) !num_choices
   with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^  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)))
+
 let mk_choice  ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl_pattern)=
   dsc,
   `Sym_interp

diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.mli b/helm/software/components/cic_disambiguation/disambiguateChoices.mli
index ddc05b4a5cba54f9c1d02a4e49883b982d6e37cf..4d1ed53296ba70c7608d396ed93303a5eebe5ddd 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateChoices.mli
+++ b/helm/software/components/cic_disambiguation/disambiguateChoices.mli
@@ -33,6 +33,9 @@ exception Choice_not_found of string Lazy.t
   (** register a new number choice *)
 val add_num_choice: Cic.term codomain_item -> unit
 
+  (** register a new number choice *)
+val nadd_num_choice: NCic.term codomain_item -> unit
+
 (** {2 Choices lookup}
  * for user defined aliases *)
 
@@ -41,6 +44,9 @@ val lookup_num_choices: unit -> Cic.term codomain_item list
   (** @param dsc description (1st component of codomain_item) *)
 val lookup_num_by_dsc: string -> Cic.term codomain_item
 
+  (** @param dsc description (1st component of codomain_item) *)
+val nlookup_num_by_dsc: string -> NCic.term codomain_item
+
   (** @param symbol symbol as per AST
    * @param dsc description (1st component of codomain_item)
    *)

diff --git a/helm/software/components/ng_disambiguation/Makefile b/helm/software/components/ng_disambiguation/Makefile
index a613a1c041645794f1e4bb90f1d937f2feb461d1..7c747df4825f9f5867dc43396ad8c7409d55cf4f 100644 (file)
--- a/helm/software/components/ng_disambiguation/Makefile
+++ b/helm/software/components/ng_disambiguation/Makefile
@@ -4,7 +4,7 @@ PREDICATES =
 INTERFACE_FILES = nCicDisambiguate.mli 
 
 IMPLEMENTATION_FILES = \
-  $(INTERFACE_FILES:%.mli=%.ml)
+  $(INTERFACE_FILES:%.mli=%.ml) nnumber_notation.ml
 EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
 %.cmo: OCAMLOPTIONS += -w Ae
@@ -41,3 +41,4 @@ depend.png depend.eps: depend.dot
 include ../../Makefile.defs
 include ../Makefile.common
 
+OCAMLARCHIVEOPTIONS += -linkall

diff --git a/helm/software/components/ng_disambiguation/nnumber_notation.ml b/helm/software/components/ng_disambiguation/nnumber_notation.ml
new file mode 100644 (file)
index 0000000..8eaa705
--- /dev/null
+++ b/helm/software/components/ng_disambiguation/nnumber_notation.ml
@@ -0,0 +1,58 @@
+(* Copyright (C) 2004, 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: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *)
+
+let error msg =
+   raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
+
+let build_nat o s str =
+   let n = int_of_string str in
+   if n < 0 then error (str ^ " is not a valid natural number number") else
+   let rec aux n = if n = 0 then o () else s (aux (pred n)) in
+   aux n
+
+let ninterp_natural_number num =
+  (*
+   let nat_URI = match Obj.nat_URI () with
+      | Some uri -> uri
+      | None     -> error "no default natural numbers"
+   in
+  *)
+   let nat_URI = NUri.uri_of_string "cic:/matita/ng/arithmetics/nat/nat.ind" in
+   let o () =
+    NCic.Const
+     (NReference.reference_of_spec nat_URI (NReference.Con (0,1,0))) in
+   let s t =
+    NCic.Appl
+     [NCic.Const
+      (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);
+;;