From: Andrea Asperti Date: Mon, 18 Jan 2010 09:50:06 +0000 (+0000) Subject: Number notation for NG. X-Git-Tag: make_still_working~3117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3b2d09d58c23757b1a50326a0ce7c355fe43d54;p=helm.git 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 59c5f5ec5..7693d8f3c 100644 --- 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 f0c7b373f..6d4d63b70 100644 --- 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 ddc05b4a5..4d1ed5329 100644 --- 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 a613a1c04..7c747df48 100644 --- 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 index 000000000..8eaa705f2 --- /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); +;;